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 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 https://frama-c.com/acsl.html