"What sets CompCert C apart from any other production compiler, is that it is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues. In other words, the executable code it produces is proved to behave exactly as specified by the semantics of the source C program... In particular, using the CompCert C compiler is a natural complement to applying formal verification techniques (static analysis, program proof, model checking) at the source code level..."
Also relevant:
"Verifiable C"
https://vst.cs.princeton.edu/
"Cyclone a safe dialect of C"
https://cyclone.thelanguage.org/
"Checked C"
https://www.microsoft.com/en-us/research/project/checked-c/
"Frama C"
https://frama-c.com/