CompCert C is a compiler designed for producing machine code for life-critical and mission-critical software written in C with high levels of assurance. It supports most of the ISO C 99 language, with some exceptions and extensions, and targets PowerPC, ARM, RISC-V, and x86 architectures. What sets CompCert C apart is its formal verification, ensuring exemption from miscompilation issues, guaranteeing exact behavior as specified by the source C program. It supports various C 2011 features and some GNU and Diab compiler extensions. The compiler is divided into three parts, with the second part being proved correct in Coq. Performance is decent, generally faster than GCC -O0 and slightly slower at higher optimization levels.
https://compcert.org/compcert-C.html