Verified Compilers

CompCert is a C compiler whose passes are written in Coq (now Rocq) and accompanied by machine-checked proofs. The proofs are then composed: each pass is shown to preserve semantics, and semantic preservation composes, so the whole chain from a formalized C subset down to assembly for several targets carries a single theorem.

The theorem is a refinement statement, and its shape is the same one [[translation-validation]] checks per compilation: if the source program is well-defined and has some observable behavior, then the compiled program has a behavior that the source was permitted to have. It says nothing about performance, nothing about code size, and nothing about programs the source semantics does not define.

It is worth being precise about the granularity of "observable". CompCert's semantics defines observable behavior as the trace of external function calls, volatile accesses and the final exit status. Ordinary memory writes to non-volatile locations are not observable, which is exactly what licenses the optimizations that exist — the same [[observable-behaviour]] boundary every compiler works within, only written down formally rather than argued about informally.

The trusted computing base of a verified compiler is much larger than the verified part, and every item in it is a place a bug can live. Naming them is not a criticism of the project — the CompCert authors name them themselves — it is the difference between using the tool correctly and holding a talisman.

The specification itself is trusted. The proof says the compiler implements *this formal semantics of C*; whether that semantics matches the ISO C standard, and whether the standard matches what you believed, is human judgement. Likewise the target semantics: the proof says the output means something specific in a formal model of the assembly language, and whether the actual processor implements that model is not a theorem.

And the practical edges are unverified for ordinary engineering reasons. Historically the parser and elaboration front end, the assembler and linker, the runtime library, and any code you link against are all outside the proof. Bugs have been found in exactly those places, which is the strongest evidence for taking the list seriously.

The reason to believe verification works here is not the existence of the proof — it is an empirical result. In the Csmith work, Yang, Chen, Eide and Regehr ran their generator against every C compiler they could obtain and found wrong-code bugs in all of them: GCC, Clang, and a long list of commercial compilers. Against CompCert they found crash and rejection bugs, and bugs in the unverified frontend — and not one wrong-code bug in the verified middle-end.

That is a much stronger statement than a proof on its own, because it was produced by the same adversarial process that found bugs everywhere else. It is also carefully bounded, and worth quoting in its bounded form: the middle-end held up under a fuzzing campaign that broke every other compiler tested. It is not a claim that CompCert has no bugs, and the authors did not make one.

The practical reading: verification eliminated a bug class, and it did so exactly where the proof applied and nowhere else. Bugs continued to appear in the unverified perimeter. That is the shape of the result, and it is also the shape of the advice — verification is a tool for removing one class of failure from one region, not a state a project reaches.

The costs are substantial and specific. The language handled is a subset — CompCert targets a large fragment of C99 rather than everything a mainstream compiler accepts, and the extensions your codebase uses may not be in it. The generated code is competitive but not state of the art: it is typically in the neighbourhood of GCC at moderate optimization, well behind a modern optimizer at its most aggressive, because every optimization must be proven and the aggressive ones are the hardest to prove. Adding a pass is a research-scale effort rather than a sprint.

So it is worth it where a miscompilation is a safety or certification problem rather than an inconvenience: avionics, rail signalling, nuclear instrumentation, medical devices. In those settings the alternative is not "a faster compiler" — it is an enormous manual review and testing burden imposed by a certification standard, and a verified compiler can displace part of that burden, which is where the economics actually come from.

For everyone else, the useful takeaway is not "use CompCert". It is that the verified middle-end result tells you where the bug class lives and that it is eliminable, and that the cheaper techniques in this module — validation, differential testing, fuzzing — are attempts to buy a fraction of the same assurance without the same cost.