Can a formally verified C compiler still miscompile your program?

Formal verification gives a compiler a machine checked refinement theorem, but that theorem governs a semantic relation rather than every component producing and executing a binary. The distinction matters whenever the verified core relies on unproved code to reify source text, realize abstract output or connect trace semantics with physical execution.

The verified development proves that successful compilation preserves observable event traces whenever source execution remains defined under its formal C semantics. This refinement result is strong, though it remains conditional on source and target models describing both the supplied program and the machine code eventually executed.

Monniaux and Boulmé’s paper maps the remaining assumptions across preprocessing, parsing, extraction, assembly printing, pseudo instruction expansion, linking, ABI conformance and the processor model. The clown reading compresses this conditional theorem into a marketing slogan, although preservation from source to execution still requires every surrounding premise to hold simultaneously.

1.Correctness scope

A compiler correctness theorem relates formal languages through labelled transition systems describing states, reductions and externally visible traces rather than concrete toolchain artifacts. Forward simulations connect typed C, lower intermediate representations, RTL and abstract assembly while proving each pass preserves the observational behavior exposed by its semantics. The proof therefore doesn't begin with source bytes on disk or end with a physical processor fetching instructions from a linked executable:

The theorem ranges over defined executions. A program that falls outside the formal C semantics is not rescued by the backend proof; definedness is a premise of trace refinement:

The verified middle remains surrounded by components preparing semantic inputs or concretizing outputs. Trusted code, axiomatized contracts and hardware behavior therefore sit outside the simulation lemma, and a defect in any of them can violate refinement from source to execution.

2.Source boundary

The development doesn't prove ISO C itself; it defines a large C99 subset with selected C11 features and verifies compilation for that formal language. Significant parts of parsing and type checking are verified, although preprocessing, the pre-parser, portions of lexing and AST elaboration remain trusted.

Whether an identifier denotes a typedef name can alter the parse itself, creating lexical feedback between symbol environments and syntactic classification. A context-free grammar can't resolve that distinction without declaration information supplied by an earlier phase already maintaining part of the scope graph. The Menhir parser is verified against an attributed LR(1) grammar, though an unverified pre-parser classifies those identifiers before the verified type checker receives the AST:

source bytes
    |
    +-- preprocessing and lexing        trusted input handling
    +-- typedef aware pre parser        trusted side condition
    +-- verified LR(1) parser           proved grammar relation
    +-- elaboration and annotation      trusted AST transformation
    `-- verified type checker           formal C invariant

The scoping witness can be written directly as C because its force is in the binding rule rather than in the editor used to display it:

/* global binding */
char t[] = {1, 2, 3};

int main(void) {
  char t[] = {1, 2, 3, 4}, s[sizeof(t)];
  return sizeof(s);
}

/* standard result: 4; reported front-end result: 3 */

A front end mismatch can remain quiet because the parser may produce a well typed formal tree whose bindings differ from the intended translation unit. Every verified pass can then preserve that unintended denotation perfectly, producing a correct proof about an AST that doesn't represent the developer's source level meaning.

The paper's witness declares global t with three elements, then introduces local t and s in the same declaration, making the scope transition itself part of the test. Under the standard, the local binding is visible to the later declarator, so sizeof(s) is four rather than the three element extent of the global object. The reported front end instead resolved sizeof(t) against the global binding and allocated three bytes, while every later verified pass remained internally consistent with that earlier mistake.

The misbinding occurs before the verified core, so every later proof can preserve the wrong denotation exactly while saying nothing about the bytes that entered the parser.

3.Extraction

Most of the compiler is implemented and proved in Coq, although the distributed executable isn't a proof term normalized directly by the kernel. Computational definitions cross a proof erasure boundary into extracted OCaml before linking with handwritten components outside the verified development, so executable behavior depends on representation choices that the logical development has erased. Consequently the extractor, host compiler, runtime and surrounding driver enter the trusted computing base for the executable that users actually invoke.

Extraction must erase proof relevant structure while preserving computational behavior for dependent definitions whose types don't translate directly into ordinary Hindley–Milner terms. The paper discusses uses of Obj.magic generated by the extractor at this representation boundary without claiming that the resulting compiler is demonstrably unsound. Correctness instead depends on extraction preserving representation invariants while the host compiler and runtime respect every erased type assumption:

The specification states that f returns at least three, and the proof of accepts_always follows immediately from that axiom. Extraction then binds f to a function returning zero, so the runtime evaluates the proved predicate to false even though the proposition was accepted by the proof environment under its stated specification.

The proof never establishes the external binding's behavior; logical consistency and executable agreement remain separate obligations at the extraction boundary.

The implementation delegates selected search problems to OCaml oracles whose certificates are accepted only after a smaller verified checker establishes the required invariant. A register allocator may therefore propose a coloring without joining the trusted base when every invalid interference assignment is rejected before affecting compilation. The paper notes that stateful or impure oracles complicate this validation firewall whenever proofs treat repeated calls as one deterministic function:

The first half of the capture demonstrates the purity problem directly: proved_equal_twice is false at runtime because two calls observe different counter states. The second half shows the safer oracle pattern, where a checker rejects invalid allocation certificates before they influence later passes.

The checker matters more than the search procedure because sound certificate rejection lets the heuristic change without modifying the acceptance theorem. This architecture only works when surrounding code can't bypass validation and when stateful helpers aren't modeled extensionally despite returning different answers across observationally equivalent calls.

Purity and identity

The sharper problem is that Coq treats a function as extensional while extracted OCaml can observe mutation, allocation identity and call history that the source semantics deliberately erase.

An oracle that increments a hidden counter can return a different result on two calls with identical arguments, violating the purity assumption used when a proof rewrites those calls as interchangeable.

The paper describes a may return monad that models such helpers nondeterministically, allowing a checker to accept any result satisfying its invariant without pretending that the external implementation is deterministic.

That approach is technically useful but invasive because every caller inherits the monadic effect, and an unsafe escape from the monad becomes another explicit trusted edge.

Representation identity creates the same issue for hash consing: two structurally equal terms can have different addresses, while pointer equality can distinguish them after extraction even though Coq identifies their values.

A smart constructor can restore the intended invariant by interning nodes and checking constructor arguments, but the hash table remains mutable state whose encapsulation must be preserved:

The identity example makes the representation gap executable: Coq proves x_eq_x = x_eq_y by reflexivity, while extracted physical equality can distinguish the two separately allocated naturals.

Finite iteration introduces a related assumption because Coq requires termination while extracted search procedures need practical fuel, defaults and error paths when a fixpoint is not reached.

A large binary encoded counter or an extracted infinite stream can implement that operational policy, although exposing pointer identity or an unexpected representation test can distinguish values that the proof treats as equal.

4.Abstract assembly

The verified backend produces an abstract assembly term rather than directly emitting final instruction bytes consumed by an assembler or processor. Its target language includes pseudo operations for frame allocation, block copies and jump tables whose denotations remain convenient for simulation proofs. Concretizing those operations into encodable instructions requires architecture specific case analysis for each opcode family, register convention and addressing mode beyond the transformation proved inside the verified backend.

Unverified OCaml code performs this expansion while the corresponding Coq definition supplies the abstract semantics that every generated sequence must implement. A forgotten clobber, mishandled register alias or out of range offset can therefore produce incorrect assembly even when every preceding transformation proof succeeds:

The paper says that printer defects emitted well formed assembly for the wrong abstract operation, including a fused multiply add with incorrectly ordered operands. Its KVX extension also printed nand as and, and the assembler accepted the result because both mnemonics were valid syntax. The second clown mistake is treating assembly acceptance as semantic validation when grammar checking can't establish correspondence with the formally proved operation.

This failure mode is difficult to isolate because the binary remains structurally ordinary and the assembler never encounters a malformed opcode requiring rejection. It instead receives a valid instruction stream whose def-use graph differs from the proved abstract program, making a printer defect surface as an incorrect numerical result.

5.Builtins

Builtins concentrate risk because they combine a compact semantic primitive with target specific selection predicates over alignment, size and register aliasing. An aligned memory copy may choose several expansions, each changing memory effects, temporary registers and clobber sets represented by the abstract specification.

The paper says that an AArch64 builtin defect generated invalid offsets and was rejected before the assembler could produce a binary. A separate register alias error affected ARM, AArch64, PowerPC and RISC V while producing code that assembled, linked and returned an incorrect result. The distinction matters because assembler rejection causes compilation failure during the build, while successful assembly can conceal a genuine compiler correctness failure that appears only in the program's observable behavior.

Clobber specifications become dangerous when register effects are duplicated between abstract semantics and handwritten target specific pseudo instruction expansion, because the two descriptions can drift without a type checker forcing them back into agreement. If the specification preserves a scratch register that expansion overwrites, verified liveness analysis may legitimately retain a live range there. The proof then validates a machine model containing a false frame condition that becomes observable once allocation exploits the supposedly surviving register.

6.Assembler and linker

The examined compiler prints textual assembly before an external assembler and linker produce the object file and final executable image. Those tools interpret instruction aliases, relocation addends, symbol bindings and section layout, making their behavior another semantic assumption between abstract assembly and execution.

A valid assembly file doesn't prove that the intended machine instruction was encoded because acceptance establishes only conformity with the assembler grammar. Relocations may resolve symbols under a different code model while section placement changes the range or interpretation of a PC relative encoding. Platform ABIs can also require callee save, stack alignment and register extension invariants absent from the machine model, which the compiler proof doesn't establish automatically.

The paper proposes direct machine code generation and verified assemblers as possible ways to reduce the conventional toolchain inside the trusted computing base. That reduction isn't free because a verified assembler must formalize encodings, relocations, object formats and the relationship between generated code and linker state. Moving the boundary inward replaces one broad external assumption with a larger formal development whose own encodings, relocation rules and object format specifications require validation before they can carry the same trust.

7.Value representations

The memory model represents pointers as allocation block identities paired with offsets, making separation, provenance and lifetime explicit within formal semantics. Physical pointers ultimately inhabit flat machine registers, so the abstraction gap returns whenever compiled code crosses an ABI boundary into separately compiled code. Depending on the calling convention, a 32 bit value in a 64 bit register may be zero extended, sign extended or retain unspecified high bits:

When caller and callee disagree about register extension, identical register contents can denote different source level values across the call boundary. The paper notes that the model doesn't formalize every ABI fact, meaning foreign function interoperability consequently depends partly on external conformance arguments. Proving one function in isolation can't establish that an arbitrary foreign callee interprets incoming registers under the same value convention.

A second KVX example concerns speculative loads producing an indeterminate intermediate value when the access was invalid under the formal memory model. The processor semantics initially returned zero, which can refine an indeterminate value closely enough for the local simulation argument to remain valid. The model is nevertheless too specific because it converts an invalid access into a predictable value that physical memory doesn't guarantee.

8.Runtime assumptions

The modeled runtime axiomatizes malloc and free through an allocator behaving as though memory were unbounded and allocation couldn't return null. This deliberate abstraction makes block based memory injections tractable, although it also makes allocation failure semantically unreachable during verified optimization. A transformation could therefore eliminate a defensive null check while preserving modeled behavior even though the corresponding execution remains possible on finite hardware:

The paper doesn't report a released optimization removing this particular check, so the example identifies a permitted semantic gap rather than an observed miscompilation. Establishing an actual defect would require a concrete compiler revision, reproducible source input and generated output demonstrating that transformation in practice.

Floating point semantics expose the same pattern because the formal model evaluates IEEE 754 operations under specified rounding while hardware and libraries mutate floating point environment state. A proof about an expression therefore depends on the surrounding environment maintaining that mode, exception behavior and every helper routine's modeled contract.

9.Processor model

Microarchitectural detail doesn't always threaten semantic correctness because hazard interlocks can enforce dependencies dynamically despite an inaccurate scheduling model. The paper examines KVX targets where an incorrect latency table introduces a stall rather than exposing a stale register value. On a non interlocked pipeline those latency assumptions become semantically relevant, allowing an otherwise identical scheduling defect to change the architectural state.

scheduler's latency view
  add r1, r2, r3       latency = 1
  mul r4, r1, r5       depends on r1

interlocked target:
  issue add; hardware stalls mul until r1 is ready

non interlocked target:
  issue add; issue mul too early and expose stale r1

This add and multiply schedule shows why correctness is parameterized by the processor's hazard relation and target specific latency semantics rather than being a property of the scheduler in isolation. The same verified list scheduler can refine an interlocked machine while failing on hardware where dependent instructions observe stale operands without automatic pipeline stalls.

10.Miscompilation

A formally verified compiler can still miscompile a program, although the qualifier matters because verified transformations aren't where the paper located its concrete defects. The reported bugs occupied trusted code surrounding the verified core, especially assembly printers, pseudo instruction expansion and synchronization between executable helpers and formal specifications. One register alias defect produced incorrect code that assembled and linked successfully, answering the question without diminishing the value of simulation proofs.

The more precise conclusion is that verified compilation reduces the surface available for miscompilation while making remaining assumptions explicit enough to inspect systematically. A conventional compiler can fail during parsing, optimization, allocation, instruction selection or printing, whereas this development proves a substantial portion of those transformations. The residual map isn't small, but it is more useful than treating formal verification as an indivisible property of an entire executable toolchain.

The end to end claim can be written plainly as a dependency list whose terms identify where semantic preservation leaves the formal development and begins relying on an external artifact. Every line is an assumption connecting one proved relation to the next concrete artifact:

end to end claim
  = proved simulations
  + correct source semantics
  + correct extraction and kernel checking
  + correct printers and pseudo expansions
  + correct assembler and linker
  + correct ABI and runtime
  + hardware matching the model

The remaining obligations are the assumptions connecting proved transformations to source text and executable machine code. Parsers require validation against the intended C standard, while printers and pseudo instruction expansions need differential testing against independently decoded instruction streams. Register clobbers and operand constraints belong in formal instruction types, while ABI and ISA models require executable validation against independent architecture semantics.

Translation validation can complement the compiler proof by checking each emitted artifact against an independent refinement relation rather than trusting every successful invocation uniformly. Verified assemblers and direct encoding can narrow the external toolchain boundary while explicit runtime contracts expose assumptions such as total allocation. These measures don't replace proofs, but they prevent an unproved concretization stage from hiding behind a theorem concerning a different intermediate representation.

11.Interpretation

The point isn't that a verified compiler has a trusted computing base because every executable system ultimately depends on assumptions outside its implementation. Dangerous components are often mundane: a printer match arm, register alias test, pre-parser classification, relocation rule or convention for unspecified register bits. These pieces look like glue even though they connect formal semantics to the concrete program that eventually executes, so a small mismatch can cross several abstraction layers before becoming visible.

Formal verification doesn't make a compiler universally infallible; it supplies a semantic contract and proves a substantial implementation against that precisely stated contract. The remaining work ensures that source parsing, generated assembly, external tools, runtime behavior and physical hardware all correspond to the objects described by the proof.

That result is considerably stronger than claiming that verification implies perfection because it identifies where failures can remain and which assumptions require independent testing. When a binary behaves incorrectly, the trusted base map shows which proof boundary the build crossed and which component must be examined next.