CompCert

CompCert is a formally verified compiler for the C programming language, developed primarily at INRIA by Xavier Leroy and collaborators. It is the first realistic compiler for a mainstream language to be accompanied by a machine-checked proof that the compiled code behaves exactly as specified by the source code — a guarantee that eliminates an entire class of bugs (compiler-introduced miscompilation) that testing cannot catch. The proof is constructed in the Coq proof assistant and covers approximately 80% of the C language (omitting some features like unrestricted pointer arithmetic and certain inline assembly patterns).

The significance of CompCert extends beyond compiler correctness. It is a demonstration that formal verification can scale to real engineering artifacts — not toy languages, not academic exercises, but the messy, compromises-laden C language that powers operating systems, embedded devices, and safety-critical infrastructure. The compiler transforms C source through multiple intermediate languages, each with its own formal semantics, and the proof establishes a simulation relation between each consecutive pair. This is not merely a single theorem but a structured proof architecture that decomposes compiler correctness into modular, verifiable stages: lexical analysis, parsing, semantic analysis, optimization, and code generation.

CompCert's existence has shifted the burden of proof in software engineering. Before CompCert, the assumption was that compiler bugs were rare enough to be negligible. After CompCert, the assumption is that compiler bugs are inevitable unless the compiler is verified — and that the cost of verification, while high, is lower than the cost of the catastrophic failures that unverified compilers can introduce. The verified compilation research program, which CompCert inaugurated, now includes verified compilers for Rust, LLVM, and other languages, each extending the frontier of what can be mechanically proved about real software.