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

Using CompCert is a natural complement to applying formal verification tech­niques (static analysis, program proof, model checking) at the source-code level. The correct­ness proof of CompCert guarantees that all safety pro­perties veri­fied on the source code automatically hold for the ge­nerated code as well.

Compilation with execution time in mind

On typical embedded processors, code generated by CompCert typi­cally runs twice as fast as code generated by GCC without optimizations, and only 20% slower than GCC code at optimization level 3. Details about the benchmark mix used to obtain these numbers are avail­able on request.

Chart of CompCert vs. GCC execution times for 23 benchmarks
Execution times of 23 benchmark programs compiled with ■ gcc -O0, ■ CompCert, ■ gcc -O1, and ■ gcc -O2

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

Supported architectures

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

Non-commercial usage

The lead developer of CompCert is Xavier Leroy with INRIA. Non-commercial usage of CompCert is free of charge.

Source code and documentation for the academic version, including the compiler proofs, can be downloaded from INRIA’s dedicated CompCert site. The source code is also hosted at GitHub.

Please note that academic releases use a different numbering scheme from commercial ones.

Commercial usage

AbsInt offers commercial li­censes, provides industrial-strength support and maintenance, and actively contributes to the advance­ment of CompCert.

To request a free trial of the latest commercial release 17.10, fill out and sign the Evaluation License Agree­ment form (PDF) and email or fax it to us.