The Cheap End of Rigour: Why Software Skipped the Middle

Software · Formal Methods · Correctness · Part I

The Cheap End of Rigour

Between “we tested it” and “we proved it” there is a long ladder. The industry climbed the first rung, glanced at the top, declared it impractical — and walked past the middle without looking.

October 2026 · Part I · How We Know Software Works

Here is a sentence written in 1970 that the industry has spent fifty-five years agreeing with and not acting on. Program testing can be used to show the presence of bugs, but never to show their absence.[1] Everyone quotes it. Almost nobody changes what they do on Monday because of it.

Think about what testing actually is. Your program accepts some space of possible inputs and moves through some space of possible internal states. A test picks one point in that space, runs it, and checks the answer. A thousand tests pick a thousand points. If the space has — and this is conservative for anything with a network connection and two threads — more configurations than there are atoms in the observable universe, then a thousand points is not a sample. It is a rounding error indistinguishable from zero.

And bugs are not distributed uniformly across that space. They cluster in exactly the regions nobody thought to sample: the boundary values, the partial failures, the interleavings, the retry that arrives after the timeout that arrives after the reconnect. The regions your tests miss and the regions your bugs live in are the same regions, for the same reason. Both are defined by what the author did not think of.

The argument in one line

There is a continuous spectrum of techniques between informal testing and full machine-checked proof. Its cheap end is now universal and invisible — you are already using it. Its expensive end is real, works, and is priced out of most projects. The middle is neither expensive nor widely used, and that is where most of the unclaimed value in software correctness currently sits.

The ladder nobody climbs

The word “formal methods” does the field enormous damage, because it sounds like a single thing you either adopt or do not — a methodology, with consultants. It is not. It is a ladder, and each rung trades effort for certainty at a different exchange rate. What follows is that ladder, from free to ruinous.

The shape of the problem. Effort rises smoothly across the ladder; adoption falls off a cliff after the third rung. The gap between them — techniques that cost days rather than years and are used by almost nobody — is the subject of this piece. Adoption is indicative, not measured.

Rung zero: you are already doing this

The most underappreciated fact in this whole area is that a type checker is a proof checker. This is not an analogy, it is a theorem — the Curry–Howard correspondence, discovered independently several times because it kept being true no matter who looked.[2] Propositions are types. Proofs are programs. Checking that a program has a type is checking that a proof establishes a proposition. They are the same activity, discovered twice by two communities who did not know they were talking to each other.

So every time your compiler accepts a program, it has proved a theorem about it. The theorem is usually boring — “this function, if it terminates, returns something shaped like a string” — but the machinery is identical to the machinery that proves an operating system kernel correct. The difference between a type checker and a proof assistant is not kind. It is only how expressive you let the propositions get.

This reframing explains something that otherwise looks like taste. When people move from a dynamically typed language to a statically typed one and report that the experience is qualitatively different rather than incrementally better, they are not being tribal. They have started getting proofs, for free, on every save. And the more expressive the type system, the stronger the theorem. Rust's borrow checker is an affine type system whose accepted programs come with a proof of no data races and no use-after-free — a genuine safety property, discharged at compile time, obtained by the average Rust programmer who has never once thought of it as mathematics. A core of that system has itself been machine-verified.[3]

The difference between a type checker and a proof assistant is not kind. It is only how expressive you let the propositions get.

Rung one: make the bad states impossible to write down

The step from “I have types” to “I use types” is where the first real return appears, and it costs nothing but discipline.

The pattern has a slogan — make illegal states unrepresentable — and a mechanism: algebraic data types, sum types, newtypes, smart constructors. Instead of a record with an optional email field and a boolean saying whether it has been validated, and a comment begging you to check the boolean, you have a type Email that can only be constructed by the validator. The invariant is no longer something you maintain. It is something the compiler maintains, at every one of the four hundred places the value is used, forever, including the ones added next year by someone who has never read your comment.

Every such move converts a runtime check that can be forgotten into a static fact that cannot. There is no other technique in mainstream programming with that cost profile. It is available in every language with a decent type system, requires no tools, no training budget, and no permission — and most codebases use perhaps a tenth of what is available.

Rung two: write laws, not examples

Ordinary tests are examples. You assert that this input gives that output, and you write as many as your patience allows. Property-based testing — QuickCheck and its very large family of descendants[4] — asks for something different: not an example, but a law.

Reversing a list twice gives you back the list. Decoding what you encoded gives you back the value. Inserting a key then looking it up finds it. Sorting produces a permutation of the input that is ordered. The tool then generates hundreds or thousands of inputs, hunting for a counterexample, and when it finds one it shrinks it — automatically simplifying the failing case until it is minimal. You do not get “failed on this 4,000-element list”. You get “failed on [0, 0]”, which usually tells you the bug on sight.

Two things make this the best-value rung on the entire ladder. The first is that the cost is barely above ordinary testing — you are writing test code, in your language, in your test runner, with no new tooling. The second is subtler and more valuable: writing a law forces you to say what your function means, not merely what it does on Tuesday. Half the bugs found by property testing are found while writing the property, before it is ever run, because the attempt to state the law reveals that you did not know what the law was.

The extension that most teams never reach is stateful or model-based property testing. You define a small, obviously-correct abstract model of your component — a dictionary standing in for a distributed cache, say — then let the tool generate random sequences of API calls and assert that the real thing and the model agree at every step. This finds ordering bugs, cache invalidation bugs and lifecycle bugs that no per-function property will ever reach, and it is still just a test suite.

Rung three: say it in the code, let a solver check it

Above laws sit contracts: preconditions, postconditions, invariants, written into the program itself. Eiffel formalised the idea as design-by-contract in the 1980s; today it lives in SPARK Ada, in Dafny[5], in JML for Java, and in refinement types for functional languages.

Refinement types are the elegant version. You do not write Int; you write “an Int that is greater than zero”, or “a list whose length equals the length of that other list”. The type system then generates proof obligations and hands them to an SMT solver — Z3, CVC5 — which discharges them automatically. Liquid Haskell[6] is the best-known instance; Dafny is the same idea built into a language designed around it.

The critical property here is automation. You write the specification; the machine finds the proof. When it works, it is close to free, and the last twenty years of SMT solver progress have made “when it works” a much larger set than it used to be. When it fails, the experience can be miserable — the solver times out, or reports failure without explaining which of your fourteen assumptions it could not establish, and you are debugging a proof search rather than a program. That unpredictability, more than the difficulty, is why this rung has not spread.

Even so, there is a version of this you can adopt today with no tooling at all: write the invariants down as assertions even if nothing checks them statically. A written invariant is a fragment of specification. It sharpens code review, it documents the thing that documentation never captures, and it is precisely the input a verifier would need if you ever decided to point one at the code.

Rung four: the rung the industry skipped

Here is the one I would put money on, and the reason this piece exists.

Everything so far verifies code. Rung four verifies the design — the algorithm, the protocol, the state machine — before the code exists. You write a model in a specification language such as TLA+[7] or Alloy[8], state the properties that must always hold, and a model checker exhaustively explores the reachable state space looking for a violation. Not samples. Every state, up to the bounds you set.

The canonical industrial account is Amazon's.[9] Engineers working on S3, DynamoDB, EBS and an internal lock manager used TLA+ on core algorithms and found bugs that had survived design review, code review, and very extensive testing by people who were unusually good at their jobs. The number that should stop you is this: one of the DynamoDB bugs required a trace of 35 steps to reproduce.

35Steps in the shortest trace reproducing a DynamoDB bug that testing and review had missed — found by model checking the designNewcombe et al., CACM 2015

0Wrong-code bugs found by three years of aggressive random testing in CompCert's verified middle endYang et al., PLDI 2011

~20:1Lines of machine-checked proof per line of C in the seL4 verified microkernelKlein et al., SOSP 2009

Sit with the 35 for a moment. No human reviewer holds 35 steps of concurrent interleaving in their head. No test suite stumbles onto that trace — the probability of randomly generating that exact sequence is effectively zero. The bug was not hard to fix; it was hard to find, and the only reason it was found is that something exhaustive went looking. Microsoft reported a similar experience on Cosmos DB, and MongoDB has published on modelling its replication protocol the same way.

Now the economics, which are the actual argument. Modelling a protocol in TLA+ takes days to a few weeks. It requires one engineer to learn a notation that is essentially set theory and temporal logic — unfamiliar, but not deep. It produces no code, ships nothing, and touches no repository. And it targets precisely the class of bug that is most expensive to find late: the distributed, concurrent, partial-failure bug that appears in production once a quarter, cannot be reproduced, and takes three engineers a week each time.

Why this rung is empty

Not cost — days, not years. Not difficulty — the notation is learnable in a fortnight. I think the real reasons are three: it produces no artefact that ships, which makes it invisible to every process that measures output; it happens at design time, which is exactly when schedule pressure is highest and the bug it prevents has not yet hurt anyone; and it is filed under “formal methods”, a phrase that makes engineering managers think of twenty-person-year kernel verifications rather than a fortnight with a state machine.

Rung five: the expensive end, and what it proved

At the top of the ladder the specification, the program and the proof all live in the same language, and “it compiles” means “it is correct”. This is the world of Rocq (formerly Coq), Lean, Isabelle/HOL, Agda and Idris. It is expensive, it is real, and the results are not toys.

Artefact	What was proved	Where it ended up
CompCert	The compiled assembly refines the semantics of the C source — no miscompilation.[15]	Csmith's random testing found 325 bugs across mainstream C compilers; in CompCert's verified middle end it found none.[10] Used in avionics.
seL4	Functional correctness of a microkernel down to the binary, plus integrity and confidentiality.	Shipping in defence, automotive and aerospace systems.[11]
Fiat-Crypto	Field arithmetic generated from a high-level specification, correct by construction.	Ships inside BoringSSL — which means inside Chrome.[12]
HACL* / EverCrypt	Memory safety, functional correctness and secret independence for crypto primitives.	Firefox's NSS, the Linux kernel's WireGuard implementation.[13]
Astrée	Absence of runtime errors, by abstract interpretation, over hundreds of thousands of lines of C.	Airbus fly-by-wire control software.[14]

And the price. seL4's original verification is usually cited at somewhere around twenty person-years for a kernel of under ten thousand lines of C, with roughly two hundred thousand lines of Isabelle proof behind it. That is a proof-to-code ratio of about twenty to one, and it is why nobody verifies a web application this way and nobody should.

But look at Fiat-Crypto again, because it is the interesting exception. It does not verify hand-written code; it generates code from a specification, with the correctness argument built into the generator. The verification effort is paid once and amortised across every curve, every platform, every future target. That is the direction in which the expensive end becomes affordable: not proving more code, but writing less of it by hand.

What it costs, what it buys

Rung	What you write	What checks it	Cost	What it catches
0 — Types	Type annotations	Compiler	Free	Shape errors, whole categories of memory bugs
1 — Illegal states	Sum types, newtypes	Compiler	Discipline only	Forgotten validation, impossible-state bugs
2 — Properties	Laws and models	Generator + shrinker	~1.2× testing	Edge cases, round-trip failures, API misuse
3 — Contracts	Pre/post/invariants	SMT solver	Days to weeks, unpredictable	Arithmetic, bounds, null, state-machine violations
4 — Models	Design specification	Model checker	Days to weeks, predictable	Concurrency, protocols, partial failure, deadlock
5 — Proof	Spec + proof + code	Proof assistant	Years	Everything the specification mentions

The honest limits

I would rather state these than have them used against the argument later.

The specification is the bottleneck, not the proof. Constructing the proof is mechanical labour, increasingly automatable. Deciding what to prove is the intellectual work — and it is the same intellectual work that makes ordinary programming hard. Formal methods do not remove the difficulty of knowing what you want. They relocate it, earlier, where it is cheaper, and make it impossible to avoid.

A proof is relative to a specification and a model. If the specification is wrong, you have rigorously built the wrong thing, and you now have a proof telling you it is fine. seL4's guarantees rest on assumptions about the compiler, the hardware model and DMA behaviour; where those assumptions fail, the theorem says nothing. Verification converts implementation bugs into specification bugs. That is an enormous improvement — specifications are shorter and more reviewable than implementations — but it is a conversion, not an elimination.

There is no universal verifier, and there cannot be. Rice's theorem settles it: every non-trivial semantic property of programs is undecidable in general. Everything practical is therefore an approximation — either incomplete (rejects some correct programs), or requiring human guidance, or bounded. Anyone selling you the general case is selling something else.

Change is expensive at the top. Refactoring verified code means redoing proofs, and proofs are notoriously brittle under change. Proof engineering — making proofs modular and robust to modification — is an active research area, which is a polite way of saying it is not solved.

The talent pool is thin. This is a genuine industrial constraint and not a point of snobbery. It also argues strongly for the middle of the ladder, where the learning curve is a fortnight rather than a doctorate.

Where the return actually is

The payoff is sharply non-uniform, and pretending otherwise is how formal methods got their reputation.

High return

Concurrency and distributed protocols, where the state space is beyond human enumeration and the bugs are irreproducible. Compilers, interpreters and anything with well-defined semantics and a wide blast radius. Cryptography, where inputs are adversarial and failure is catastrophic. Safety-critical control. Consensus, replication, cache coherence. Anything with a small, stable, precisely statable core.

Low return

CRUD applications. User interfaces. Anything where the requirements are genuinely unknown and the point of building is to discover them. You cannot prove conformance to a specification that does not exist yet, and writing one prematurely is worse than useless — it is expensive and it is wrong.

The diagnostic is two questions. Do I know precisely what correct means? And does being wrong cost a lot? Two yeses and the middle of the ladder is a bargain. One no and you are probably better off shipping and finding out.

What I would actually do

Concretely, in order of return on effort:

One. Use the strongest type system available to you, and use it to make illegal states unrepresentable rather than merely to catch typos. This is free and most codebases leave nine-tenths of it on the table.

Two. Replace example-based tests with property-based tests wherever a law exists. Start with round-trips (decode(encode(x)) == x) and invariants — they are the easiest to find and they catch the most. Then reach for stateful property testing on your one genuinely stateful component.

Three. Write invariants down as assertions even where nothing checks them statically. You are producing specification fragments, cheaply, as a side effect of work you were doing anyway.

Four. For any concurrent or distributed design — a protocol, a state machine, a locking scheme, a migration with a cutover — model it before you implement it. This has the best cost-to-benefit ratio of anything on this list and it is the step almost nobody takes.

Five. Reserve full verification for a small, stable, high-stakes core: a parser, a state machine, a crypto primitive, a permission check. Leave the periphery conventional. The mistake is treating verification as an all-or-nothing property of a system rather than a property you buy for the parts that warrant it.

So: is there a more mathematical way to develop software than the traditional one? Yes, unambiguously, and it has been shipping in aircraft, kernels and browsers for two decades. But the interesting fact about the industry is not that it rejected formal methods. It is that it silently adopted the cheap end — static types, borrow checking, property testing, SMT solvers humming away inside tools nobody thinks of as verifiers — while walking straight past the middle, where a fortnight's work on a state machine would have prevented the outage that cost the quarter.

Part II follows. This piece treated correctness as something you prove. There is an older and stranger tradition that treats it as something you see — where a deadlock is a hole you cannot walk around, a loop nest is a solid you rotate, and the impossibility of distributed consensus is a fact about connected spaces. The Shape of the Problem takes the geometric view.

References

1. Dijkstra, E. W. (1970). “Notes on Structured Programming”, EWD249; see also “The Humble Programmer”, Communications of the ACM 15(10), 859–866 (1972).
2. Wadler, P. (2015). “Propositions as Types.” Communications of the ACM 58(12), 75–84. dl.acm.org
3. Jung, R., Jourdan, J.-H., Krebbers, R. & Dreyer, D. (2018). “RustBelt: Securing the Foundations of the Rust Programming Language.” POPL 2018. plv.mpi-sws.org
4. Claessen, K. & Hughes, J. (2000). “QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs.” ICFP 2000.
5. Leino, K. R. M. (2010). “Dafny: An Automatic Program Verifier for Functional Correctness.” LPAR-16.
6. Vazou, N., Seidel, E., Jhala, R., Vytiniotis, D. & Peyton Jones, S. (2014). “Refinement Types for Haskell.” ICFP 2014.
7. Lamport, L. (2002). Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley.
8. Jackson, D. (2006). Software Abstractions: Logic, Language, and Analysis. MIT Press.
9. Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M. & Deardeuff, M. (2015). “How Amazon Web Services Uses Formal Methods.” Communications of the ACM 58(4), 66–73. dl.acm.org
10. Yang, X., Chen, Y., Eide, E. & Regehr, J. (2011). “Finding and Understanding Bugs in C Compilers.” PLDI 2011.
11. Klein, G. et al. (2009). “seL4: Formal Verification of an OS Kernel.” SOSP 2009; extended as “Comprehensive Formal Verification of an OS Microkernel”, ACM TOCS 32(1), 2014.
12. Erbsen, A., Philipoom, J., Gross, J., Sloan, R. & Chlipala, A. (2019). “Simple High-Level Code for Cryptographic Arithmetic — With Proofs, Without Compromises.” IEEE S&P 2019.
13. Zinzindohoué, J.-K., Bhargavan, K., Protzenko, J. & Beurdouche, B. (2017). “HACL*: A Verified Modern Cryptographic Library.” ACM CCS 2017.
14. Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D. & Rival, X. (2003). “A Static Analyzer for Large Safety-Critical Software.” PLDI 2003.
15. Leroy, X. (2009). “Formal Verification of a Realistic Compiler.” Communications of the ACM 52(7), 107–115.

Published October 2026 · Part I of How We Know Software Works · Part II: The Shape of the Problem.

On method and tools

This piece was written collaboratively with Claude Opus 5 (Anthropic): human specification and critical review, machine synthesis and drafting. Claims about verified systems are cited to the primary papers rather than to secondary summaries, and the effort figures for seL4 are given as the approximations they are — published totals vary with what is counted as verification work. Where the argument is my opinion rather than the literature's finding — principally the claim that the fourth rung is the industry's largest missed opportunity — it is marked as such.

The uncomfortable part of this subject is that the hard step was never the proof. It was always saying precisely what you wanted.

Authored by: Luis Matos Ferreira
Physicist & Developer