CompCert is a formally verified optimizing C compiler for safety-critical and mission-critical software. Unlike any other production compiler, it is mathematically proven to be exempt from miscompilation issues. Such confidence in the correctness of the compilation process is unprecedented and helps meet the highest levels of software assurance
- 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. The correctness proof of CompCert guarantees that all safety properties verified on the source code automatically hold for the generated code as well.
- On typically embedded processors, the code generated by CompCert typically runs twice as fast as the code generated by GCC without optimizations, and only 20% slower than GCC at optimization level 3.