Frama-C lets you prove all sorts of useful properties about C code, including memory correctness. (Actually writing the proofs is a lot of work though.)

https://frama-c.com/acsl.html