Successes have been claimed.[1]
It's discouraging to me how little progress there's been in proof of correctness in the last 35 years. I used to work on that stuff. C set the field back by decades.
[1] https://books.google.com/books?id=yvJqCQAAQBAJ&pg=PA364&lpg=...
That was one of the "toy" implementations I mentioned. The algorithm they described is going to be nowhere near the performance of a modern multithreaded allocator like jemalloc (which is correspondingly far more complex). Which is not to say things like that are not encouraging, only that I was hoping someone would have proven something people actually use correct.
Unfortunately, having actually looked for production strength proofs of correctness for production allocators (as opposed to toys), I wasn't able to find any. Given how high-value of a target they are for formal verification, we may be underestimating the complexity of doing so.