For thirty years formal verification was something that happened in papers about systems nobody ran.
Two things changed that. seL4 produced a verified kernel that is deployed in real safety- and security-critical systems. And the tooling reached the point where an ordinary engineer can apply it to a bounded problem without a doctorate in the subject.
The spectrum, because "formal methods" covers very different things¶
These are worth separating, because the cost and the payoff differ by orders of magnitude:
- Type systems. The formal method everyone already uses without calling it one. A compiler rejecting a type error is a proof of a property. Rust's borrow checker is the same trick with a stronger property attached.
- Property-based testing. Not proof; it generates cases against invariants you've stated. Cheap, and it finds a surprising proportion of what proof would.
- Model checking. Exhaustively explore a finite state space. TLA+ is the practical entry point and has the best industrial track record, particularly for distributed protocols where the bugs live in interleavings nobody imagined.
- Deductive verification. Prove a program satisfies a specification. Expensive, and what seL4 did.
Most of the value on offer sits in the first three. The fourth is for things where failure is unacceptable.
What seL4 demonstrated¶
Not that verification is cheap. The original effort was famously on the order of twenty person-years for about ten thousand lines.
What it demonstrated is that it's possible at all for real systems code, and that the proof can be maintained. The proofs have been carried forward across new architectures: 32-bit Arm first, then x86-64 and 64-bit RISC-V, with AArch64 and the MCS configuration both in progress as of this writing (seL4 news). A proof that rots the first time you modify the code would be a curiosity. One that survives a port is an engineering artefact, in the way that a bridge design you can reuse is an engineering artefact.
Once the proof is an engineering artefact, a whole class of argument gets settled once and then reused.
Take a railway signalling interlock, a battery management controller, an infusion pump. Today each is certified by process: documents, review boards, test campaigns, a trail of paper establishing that competent people were careful. That is expensive, it has to be redone for every variant and it produces confidence rather than proof.
A verified kernel underneath changes what has to be argued. Our bet is that this is where the money goes next: not proving applications correct, which will stay out of reach, but proving the separation between them, so a safety case can be made about one component at a time instead of about the whole box. That is the difference between recertifying a medical device because the Wi-Fi stack changed and not having to.
For engineering itself, the class of bug that disappears is the one nobody can reproduce. A proof covers every execution, including the interleaving that happens once a fortnight on one customer's hardware and never on your bench.
The limits¶
- A proof is relative to a specification. If the spec is wrong, the proof is worthless and you now have high confidence in the wrong thing. Writing the spec is where the thinking lives.
- Assumptions matter enormously, and seL4 names its own. The proofs assume the hardware behaves as modelled, and exclude the boot process, the low-level assembly the kernel starts from, direct memory access by peripherals and timing channels. Spectre was the hardware not behaving as modelled, which is the first of those assumptions failing in public. "Formally verified" means verified against that model and those exclusions, and anyone quoting it as a general separation guarantee has dropped the half that matters.
- Cost scales badly with size. This is for kernels, protocols and crypto primitives, not for application code.
Reusing a proof is cheap. The small labour market able to make one is not.
There are perhaps a few hundred people in the world who can carry a functional-correctness proof through a non-trivial port. They are expensive, they are concentrated in a handful of research groups and a handful of large companies, and the companies are the ones who can also afford to wait three years for the result. If verification becomes the thing that distinguishes a certifiable product from an uncertifiable one, then the ability to produce a verified component is a competitive moat held by whoever employs that cohort.
The optimistic reading is that proofs are artefacts, and an artefact can be published. seL4's proofs are open, which means a small team can build on top of a verified kernel without employing a single proof engineer. That is a different distribution of power from the one where the verified component ships as a binary blob under a per-seat licence with the proof held as commercial confidence. Both futures are available right now and the licence terms decide which one you get.
Here at AxisOps we will take the open one, and the reason is practical rather than ideological: a proof you are not allowed to read is a claim, and a claim is what verification was supposed to replace.
The practical recommendation¶
The highest-value thing most teams could pick up is TLA+ for distributed protocol design, used before implementation. Distributed systems bugs live in interleavings, interleavings are what model checking explores exhaustively, and a design bug found before implementation is the cheapest bug there is.
That's a days-to-weeks investment, not twenty person-years.