What Has Actually Been Verified, and What It Cost

Verification is easy to discuss in the abstract and easy to dismiss as impractical. Two projects settle the question of feasibility, because both produced machine-checked proofs about code that runs.

CompCert is a formally verified optimising C compiler, described by Xavier Leroy in "Formal verification of a realistic compiler", Communications of the ACM, volume 52, issue 7, 2009, pages 107 to 115. Its theorem is a semantic preservation result: the generated assembly behaves as the source C program's semantics specify.

seL4 is a formally verified operating system microkernel, presented by Gerwin Klein and colleagues at SOSP in 2009. Its theorem is functional correctness: the C implementation refines an abstract specification.

Both are real. CompCert compiles real C and is used where compiler-introduced bugs are unacceptable. seL4 is a working microkernel.

So the question is not whether this is possible. It is what it costs, and both projects published enough to answer that precisely.

The seL4 team published their effort in detail, and the figures are the most useful data point in the field precisely because they are unflattering.

kernel implementation      8,700 lines of C  +  600 lines of assembler
proof                    ~200,000 lines of Isabelle script
                         (~165,000 written by hand)

implementation effort    ~30 person-months
proof effort             ~20 person-years
                         (~11 py attributable to seL4 itself;
                          the rest went into reusable libraries)

Two ratios follow, and both are worth sitting with.

The proof is roughly 23 lines per line of code, or 19 counting only what was written by hand.

The effort ratio is starker: 20 person-years of proof against about 2.5 person-years of implementation, so roughly eight times as much work went into proving the kernel as into building it.

The parenthetical matters for anyone extrapolating. Around 9 of those 20 person-years produced reusable infrastructure, so a second project of similar kind would not pay it again. The marginal cost is closer to 11 person-years, which is still more than four times the implementation.

A verified system still rests on assumptions, and being precise about them is what separates an honest claim from marketing.

Everything a proof depends on but does not establish is the trusted computing base. For a verified kernel it typically includes:

The specification. The proof says the code matches the spec. If the spec is wrong, the proof is intact and the system is wrong.

The proof checker. Isabelle's kernel must be correct. It is small and heavily scrutinised for exactly this reason, and it is still trusted rather than proved.

The hardware. The proof assumes the processor implements its documented semantics, and that memory holds its contents.

Whatever the model omits. The original seL4 proof did not cover hand-written assembly, the boot code, or hardware-managed caches and timing behaviour.

Note what these have in common: they are all enumerable. That is the real achievement. In an unverified system the assumptions are unbounded and unknown; in a verified one they are a short, written list you can inspect and argue about.

Moving from "we believe this is correct" to "this is correct provided these six things hold" is a genuine change in kind, even though it is not the absolute guarantee the word proof suggests.

CompCert's value is easy to underestimate until you notice where it sits in the stack.

Every other verified artefact is verified as source code. It then passes through a compiler, which rewrites it aggressively, and the machine executes the compiler's output rather than the thing that was proved.

So an unverified compiler is in the trusted computing base of every verified program on the system. A miscompilation silently invalidates the proof, and the proof gives no warning because it was never about the binary.

CompCert closes that specific gap. Its semantic preservation theorem states that the generated assembly behaves as the source program's semantics permit, so a property proved of the source carries down to what actually runs.

This is the general shape of how verification composes: each verified layer removes itself from the layer above's trusted base. Verified compiler plus verified kernel plus verified application is worth more than the sum, because each one shrinks what the others must assume.

It also explains why compilers and kernels were done first. They are the layers everything else trusts, so verifying them pays a dividend across every program that runs on top.

Two questions decide it, and the second is the one people skip.

Cost of failure is the obvious gate. Where a bug can be fixed by deploying again on Tuesday, an eightfold effort multiplier is indefensible. Where the artefact goes into a satellite, a medical device or a chip, or where a compromise is unrecoverable, the arithmetic changes completely.

Specification stability is the gate that kills projects. A proof is written against a specification, and changing the specification invalidates proofs. A component whose requirements change every sprint cannot carry a proof, because the proof is re-done each time. This, more than difficulty, is why verification concentrates in kernels, compilers, protocols and hardware: those specifications are stable for years.

The final box is the practical form. Nobody verifies a product. They verify the small core where the critical invariants live, and rely on ordinary engineering everywhere else. seL4 is 8,700 lines, which is a kernel rather than an operating system.

Choosing that core well is most of the skill.

Full verification is the expensive extreme, and the same ideas are available at every price point. Most of the value is not at the extreme.

Types. Every property pushed into a type is a proof the compiler checks for free, and the previous lesson's transferable question applies in any typed language: can this be made unrepresentable rather than checked?

Assertions and contracts. Writing preconditions, postconditions and invariants as executable checks costs almost nothing, catches violations at runtime, and, crucially, is the same artefact a verifier would consume later.

Property-based testing. Stating a property and having a tool generate inputs against it is dramatically cheaper than proof and finds a large share of what proof would find. It samples rather than covers, and shrinks failures to minimal cases.

Model checking the protocol. Days of effort on the concurrent core, per the previous lesson, catches the bugs testing structurally cannot.

Sound static analysis. Tools proving the absence of specific defect classes are proofs with the specification fixed in advance, requiring no annotation.

Read as a ladder, the practical advice is to climb it rather than jump. Each rung is cheaper than the next and catches a different class of error, and the marginal value of the top rung is only large when failure is genuinely unrecoverable.

The fifth row is the one to take away. A verified system's guarantee is not absolute correctness; it is that the remaining risk has been moved into an enumerated list.

That is a genuine change. An unverified system's assumptions are unbounded and mostly unknown, so "what could go wrong" has no answer. A verified one's assumptions are written down, and each can be examined, argued about, or removed by verifying another layer.

The honest summary of the whole path: verification does not eliminate uncertainty, it relocates it from the implementation into the specification and the trusted base, both of which are far smaller and far more scrutable than the code was.

Whether that relocation is worth eight times the effort is an engineering judgement, and the two questions from the decision diagram answer it in most cases without any theory at all.

Four lessons, three traditions, one boundary.

Deductive proof turns a program into a relation between assertions, and the loop invariant is the step no machine can supply, which is Rice's theorem showing up as a daily engineering constraint. Type-level encoding removes the gap between spec and code by making them the same artefact, paying for it with a total language. Model checking abandons proof for exhaustive search, which is decidable because the state space is finite, and is limited by exactly that finiteness.

Each hits a different wall, which is why none replaced the others and why real systems use all three at different layers.

The transferable habit is the question the decision diagram asks: what does failure cost, and how stable is the specification? Those two answers place a component on the ladder from tests to types to model checking to proof, and they are answerable without knowing any of the theory.

And the general lesson, which outlasts any of these tools: correctness is always relative to a specification. Every technique here verifies agreement between two artefacts. None of them can tell you that you asked for the right thing, and that remains the hardest and least automatable part of building software.