Compcert guarantees that the executable that comes out does what the code that went in said, it doesn’t guarantee much about the code that went in.

There's also Frama-C, but having used both Frama-C and SPARK I can say I'd pick SPARK any day. Having a rich type system and not having to work with pointers makes proving a program so much easier.

Right, Frama-C can formally prove properties of C code.

There are also proprietary solutions that do something similar:

• https://www.eschertech.com/products/ecv.php

• https://www.trust-in-soft.com/