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 PowerPC, x86, ARM, AArch64, and RISC-V architectures.

What sets CompCert apart?

ACM Software System Award

CompCert is the only production compiler that is formally verified, using machine-assisted math­ematical proofs, to be exempt from mis­compilation issues. 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 was 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.”

In 2022, the Association for Computing Machinery, ACM, presented the CompCert development team with the prestigious ACM Software System Award. Subsequently, the team also received the ACM SIGPLAN Programming Languages Software Award.

Formally verified optimizations

CompCert implements the following optimizations, all of them formally verified:

Who uses CompCert?

The Institute of Flight System Dynamics at the Technical University of Munich uses CompCert in the development of flight control and navigation algorithms.

In 2017, CompCert was successfully qualified by MTU Friedrichshafen according to IEC 60880, category A, and IEC 61508-3:2010, SCL 3 for a certification project in the nuclear energy domain. The use of CompCert reduced development time and costs.

Airbus France is deploying CompCert at the Toulouse plant in a number of currently undisclosed projects.

In the civil-aviation research project QSMA by the German Federal Ministry for Economic Affairs and Energy, CompCert is being used to develop a TSO-C151b Terrain Avoid­ance and Warning System in accordance with DAL-C. The project is carried out by emmtrix, the German Aerospace Center DLR, Validas, TU Clausthal, and AbsInt.

Your benefits

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.

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, 2016

The computed WCET bounds lead to a total processor load which is about 28% smaller with the CompCert-generated code than with the code generated by the conventional compiler. The main reason for this behaviour is the improved memory performance. The result is consistent with our expectations and with previously published CompCert research papers.”

MTU Friedrichshafen, 2018

Supported architectures

CompCert produces machine code for PowerPC (32-bit and 32/64-bit hybrid), IA32 (x86 32-bit), AMD64 (x86 64-bit), ARM and AArch64, and RISC-V (32- and 64-bit).

Supported tool chains

To preprocess and produce object and executable files, an external C preprocessor, assembler and linker have to be provided. CompCert is currently tested for compatibility with:

GNU logo DiabData logo

An optional tool called Valex is available for the postpass validation of the assembling and linking steps. It compares the instructions in the abstract assembly code produced by CompCert to the instructions in the linked binary executable, checks whether symbols are used consistently, whether variable size and initialization data match up, and whether variables are placed in the proper sections in the executable.

Free trial

Request your free trial package today.

Watch on YouTube

Introduction to CompCert

A recording of a joint webinar with Vector Informatik held on 8 June 2021.

  • Terminology: Compiler validation vs. compiler verification
  • Introduction to formal compiler verification
  • Benefits of formally verified compilation
  • Experimental evaluation of CompCert performance
  • Tool qualification strategy for industry norms such as ISO 26262

ACM Software System Award 2021

The 2001 Award goes to the CompCert developer team: Xavier Leroy, Sandrine Blazy, Zaynah Dargaye, Jacques-Henri Jourdan, Michael Schmidt, Bernhard Schommer, and Jean-Baptiste Tristan.