Formally verified compilation

CompCert is a formally verified optimizing C compiler. Its intended use is compiling safety-critical and mission-critical software written in C and meeting high levels of assurance. It ac­cepts most of the ISO C 99 language, with some exceptions and a few extensions. It produces machine code for ARM, PowerPC, and x86 architectures.

What sets CompCert apart?

Unlike any other production compiler, CompCert is formally verified, using machine-assisted math­ematical proofs, to be exempt from miscompilation issues. In other words, the code it pro­duces is proved to behave exactly as specified by the semantics of the source C program.

This level of confidence in the correctness of the compilation process is unprecedented and con­tributes to meeting the highest levels of software assurance.

CompCert diagram

The formal proof covers all transformations from the abstract syntax tree to the generated assem­bly code. To preprocess and produce object and executable files, an external C pre­processor, assemblers, linkers, and C libraries have to be used. However, these unverified stages are well-understood and robust from an implementation perspective. This has been demon­strated on a devel­op­ment version of CompCert in a 2011 study by Regehr, Yang et al.:

The striking thing about our CompCert results is that the middle-end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task. The apparent unbreak­ability of CompCert supports a strong argument that developing compiler optimizations within a proof framework, where safety checks are explicit and machine-checked, has tangible be­ne­fits for compiler users.”

Your benefits

With CompCert it is possible to decrease the execution time of our flight control algo­rithms by a sig­nif­icant amount. The reduction of the execution time can be used for additional functionality.”

TU Munich, Institute of Flight System Dynamics

Availability

CompCert produces machine code for ARM, PowerPC (32-bit), and IA32 (x86 32-bit).

The lead developer of CompCert is Xavier Leroy with INRIA. Non-commercial usage of CompCert is free of charge. AbsInt offers commercial li­censes, provides industrial-strength support and maintenance, and actively contributes to the advance­ment of the tool.

Source code and documentation (including the compiler proofs) can be downloaded from INRIA’s dedicated CompCert site.

The source code is also hosted at GitHub.