CompCert
The only fully verified C compiler with mathematical proof of correctness Formally verified and mathematically proven
CompCert is a formally verified optimizing C compiler supporting several processor architecture and tool chains.
Mathematically Verified Compiler
CompCert is the only C compiler that comes with a mathematical proof that the generated assembly code behaves exactly as specified by the semantics of the source C program.
CompCert is the only C compiler that comes with a mathematical proof that the generated assembly code behaves exactly as specified by the semantics of the source C program. Its intended use is compiling safety-critical and mission-critical software written in C and meeting high levels of assurance. It accepts most of the ISO C 99 language, with some exceptions and a few extensions. It produces machine code for many architectures.
What sets CompCert apart?
CompCert is the only production compiler that is formally verified, using machine-assisted mathematical proofs, to be exempt from miscompilation issues. The code it produces 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 contributes to meeting the highest levels of software assurance.
The formal proof covers all transformations from the abstract syntax tree to the generated assembly code. To preprocess and produce object and executable files, an external C preprocessor, assemblers, linkers, and C libraries have to be used. However, these unverified stages are well-understood and robust from an implementation perspective. This was demonstrated on a development version of CompCert in a 2011 study by Regehr, Yang.
Features
Key Features
- Mathematically proven correctness
- High optimization performance
- Industry-standard C support
- Supports multiple architectures
- Qualification evidence available
Supported Architectures
- PowerPC (32-bit)
- ARM (32-bit)
- x86 (32-bit)
- RISC-V (32 and 64-bit)
Formally verified optimizations
CompCert implements the following optimizations, all of them formally verified:
- Register allocation using graph coloring and iterated register coalescing
- Instruction selection with strength reduction, to take advantage of combined instructions provided by the target architectures
- Constant propagation for integer and floating-point types
- Common subexpression elimination
- Dead code elimination
- Redundant code elimination
- Function inlining
- Tail call elimination
- •If-conversion
Experience Verified Compilation
Join leading companies using CompCert for their mission-critical software