CompCert: A C Compiler That Comes With a Proof

Safety-critical teams put considerable effort into their C source code. They run static analysis, check MISRA rules, review code, and test the compiled software extensively. However, testing cannot cover every execution path or guarantee that the compiler itself hasn't introduced errors. In avionics, rail, or nuclear software, this raises an important question: how can we trust the compilation process?

What Is CompCert?

CompCert is a formally verified optimizing C compiler developed at INRIA by Xavier Leroy and his team, and commercially supported by AbsInt. Designed for safety-critical and mission-critical applications, it supports architectures including PowerPC, Arm, AArch64, x86, and RISC-V.

CompCert is a C compiler, not a C++ compiler. It supports ISO C99, selected C11 features, and the MISRA-C 2004 language subset, with certain documented restrictions.

What Does Formal Verification Mean?

A compiler performs several transformations to optimize and translate C code into assembly, but each transformation introduces a possibility of errors, known as miscompilation.

CompCert addresses this through 15 verified compilation passes across eight intermediate languages. Each pass comes with mathematical proofs demonstrating that its transformations preserve the permitted behaviour of the original program.

These proofs are checked using Rocq (formerly Coq), a mathematical proof assistant that verifies the logical correctness of the reasoning. Unlike conventional testing, which examines selected inputs and execution paths, these proofs establish correctness for all cases covered by the formal model.

This property, known as semantic preservation, helps ensure that generated assembly preserves the behaviour of the original C program. CompCert therefore complements source-level static analysis and software testing by providing additional assurance about the compilation process itself.

Working with Existing Toolchains

CompCert's core optimizations and code-generation algorithms are formally verified, while external stages such as preprocessing, assembling, and linking rely on toolchains such as GCC or Wind River Diab.

For additional assurance, AbsInt offers Valex, a separate tool that validates aspects of the final executable against the assembly produced by CompCert.

The Csmith Result

In a 2011 study, researchers used Csmith to generate random C programs and uncover more than 325 previously unknown compiler bugs.

CompCert stood out as the only compiler tested for which Csmith could not find wrong-code errors in the development version examined, despite approximately six CPU-years of testing. While not proof that CompCert is entirely bug-free, the result demonstrated the benefits of formally verified compiler optimizations.

How Does CompCert Compare With GCC?

CompCert combines formally verified compilation with optimizations such as register allocation, constant propagation, dead code elimination, and function inlining.

Published benchmarks report CompCert-generated code running approximately twice as fast as GCC at -O0, around 10% slower at -O1, and 20% slower at -O3, depending on the workload and processor.

Unlike GCC, CompCert treats -O1, -O2, and -O3 as equivalent speed-optimization options, while -Os focuses on code size. Its key advantage is combining practical optimization with mathematically verified compilation.

A Major Avionics Milestone: CompCert's 2026 ATR Qualification

In 2026, CompCert was successfully qualified for the Multi-Function Computer New Generation (MFC_NG) of ATR 42/72 aircraft, supporting certification credits under DO-178C, DO-333, and DO-330.

Under appropriate qualification conditions, these credits can help reduce or replace certain object-code verification activities with source-level formal verification, potentially reducing certification effort.

CompCert also has an established industrial history, including deployment by Airbus France at its Toulouse facility and qualification for a nuclear-sector project by MTU Friedrichshafen in 2017.