CompCert and the Verified Compiler: Proving the Translator Correct
CompCert used Coq to prove semantic preservation across a realistic optimizing C compiler, closing the assurance gap between verified source programs and generated assembly.
Verifying source code leaves a compiler-sized hole in the assurance argument
A formally verified source program is not what a processor executes. A compiler transforms it through parsing, intermediate representations, optimization passes, code generation, assembly, and linking. If that translation silently changes behavior, a proof about the source may no longer justify the executable.
Xavier Leroy’s CompCert project attacked this gap by building a realistic optimizing C compiler whose semantic-preservation theorem is machine-checked with Coq.[1][2]
CompCert states compiler correctness as semantic preservation
The central theorem relates a source program to the assembly program produced by the compiler. CompCert’s manual states the high-level property in terms of observable behaviors: when compilation succeeds, the generated code preserves the behaviors allowed by the source semantics.[3]
This is stronger than testing a compiler on many examples. The proof ranges over all programs covered by the formal language and the verified compilation passes under the stated assumptions.
The theorem needs formal semantics on both sides
A semantic-preservation proof requires precise definitions of the source language, intermediate languages, and target assembly behavior. Verification therefore forced CompCert to make language meaning explicit instead of relying on an informal understanding of C and machine code.
The compiler is structured as a chain of verified transformations
Compilers are easier to verify when translation is decomposed into passes between intermediate representations. Each pass can have a theorem showing that the target representation simulates or preserves the relevant behavior of its input.[2]
The overall compiler theorem then follows by composing correctness results across the pipeline. This mirrors compiler engineering itself while turning every optimization into a proof obligation.
Optimization made the project more historically significant than a toy translator
CompCert was designed as an optimizing compiler for a substantial subset of C, not merely a direct syntax-to-assembly demonstrator. Leroy’s 2009 Communications of the ACM article described it as a realistic compiler whose semantic preservation was proved using Coq.[1]
This distinction matters because compiler bugs often occur precisely in optimization: an apparently valid algebraic or control-flow transformation may fail for a corner case the implementer did not anticipate.
A verified optimizer must prove when a transformation is legal
Optimization is no longer justified by ‘these expressions look equivalent.’ The proof must account for the language semantics, memory model, undefined behaviors, and control flow conditions under which the rewritten program preserves the required observations.
Coq served as both specification language and proof checker
Much of CompCert’s implementation and correctness development is expressed inside Coq. The project’s documentation provides a commented listing of specifications and proofs, making the verification artifact inspectable rather than reducing assurance to a certificate from a closed tool.[2]
This close integration allowed executable compiler components to be extracted from formally defined functions while the theorems about those functions remained connected to the same definitions.
The verified back end demonstrated proof at realistic compiler scale
Leroy’s Journal of Automated Reasoning paper described a formally verified back end from an intermediate language to PowerPC assembly, including register allocation and code-generation machinery representative of a serious compiler.[4]
The project showed that large compiler proofs could be maintained as engineered artifacts. That was an important step beyond proofs of tiny language fragments whose implementation complexity did not resemble production compilers.
The trusted computing base did not vanish
CompCert’s theorem does not prove every layer of a deployed system. Parsing, preprocessing, assemblers, linkers, hardware, operating systems, and the proof assistant’s trusted kernel remain relevant depending on the exact toolchain and theorem statement. Formal verification narrows and identifies assumptions rather than erasing them.
Testing still found a striking difference between verified and unverified compilers
Research comparing compiler behavior found wrong-code bugs in mainstream compilers and famously reported no wrong-code bugs in the verified portions of CompCert during the tested period. Such experiments are not themselves a proof of CompCert, but they illustrate the practical value of eliminating classes of optimizer defects through formal verification.[5]
The important methodological point is that testing and proof answer different questions. Random differential testing can discover unexpected defects; a semantic-preservation proof establishes a universal relationship within its formal scope.
Verification can shift bugs toward the specification boundary
When an implementation is tightly proved against a formal semantics, remaining mistakes are more likely to involve the formal model, unverified components, or misunderstood source-language behavior. Assurance work therefore becomes more focused rather than unnecessary.
CompCert evolved as both research result and maintained compiler.
The project has continued to support additional architectures and releases. Its current documentation describes generation for ARM, PowerPC, RISC-V, and x86, while preserving Coq-checked semantic correctness for the verified compiler pipeline.[2]
Long-term maintenance matters historically because it demonstrates that proof artifacts can evolve with code instead of becoming obsolete immediately after publication.
Why CompCert changed expectations for verified software tools
CompCert showed that the compiler itself—the tool trusted to turn proved source into machine code—could be subjected to machine-checked verification at realistic scale. The semantic-preservation theorem closes a major link in end-to-end software assurance.[1][3]
It did not make every C program correct, and it did not verify every external tool. Its achievement was narrower and more important: when a supported source program is compiled successfully, the compiler’s own optimizations are backed by a mathematical proof that the generated assembly preserves the specified behavior.
Works Cited
- 01
- 02
- 03CompCert Manual — Semantic Preservation Theorem compcert.org
- 04
- 05
CodeHistory is a living archive. Citations document the evidence used for this edition; later evidence may refine the account.
Submit a research lead