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: