They prove a lot more, e.g. that if you have an oracle that can guess the total amount of memory needed beforehand, during runtime the malloc call will never fa

They prove a lot more, e.g. that if you have an oracle that can guess the total amount of memory needed beforehand, during runtime the malloc call will never fail if you stay under the amount. But of course it's rabbit holes all the way. Whatever application uses this allocator also needs to be verified, where then you need to prove that there is never a sequence of malloc/free calls that will exceed this limit.