The phrase is doing too much work
When one engineer says "formal verification" to another, there are about eight things they could mean, and the cheapest and most expensive are two orders of magnitude apart in effort. Half the room hears a machine-checked proof of functional correctness against a mathematical specification, which for an operating system kernel took a research group most of a decade. The other half hears a property-based test that generates a thousand random inputs and shrinks the failure. Both are on the same ladder, and a conversation that does not name the rung produces a bad decision. At the bottom the honest answer is that you already do this and should do more. At the top, for almost every commercial system, it is no.
You are probably here because
- The same failure has hit production twice and has never once happened on a laptop, and the postmortem ends with "could not reproduce"
- The suite is green and coverage is high, and the defects that reach customers are all ordering, timing and failover bugs nobody wrote a test for
- Someone said "we should use TLA+" in a meeting and nobody in the room could say what it would cost or what it would prove
- Nobody can write down in one sentence what the system must never do, and three people give three different answers
These usually share one root cause — the defect lives in an interleaving your tests sample at random and almost never reach, and the invariant was never written down anywhere — which is what Three problem shapes where it pays and The specification is the deliverable, below, are about.
Here is the ladder we use, bottom to top. Each rung buys a stronger claim and costs more, and the jump is not smooth. There is a cliff between rung five and rung six that most teams never need to cross.
Types and totality. The compiler proves a small theorem about every expression you write. Sum types that make an invalid state unrepresentable, non-nullable references, ownership and lifetimes in Rust, exhaustiveness checking on a match. This is verification, it runs in under a second, and most codebases use maybe a third of what their own type system already offers.
Contracts and assertions. Preconditions, postconditions, invariants checked at runtime. Cheap, and they turn a silent corruption into a loud crash near the cause instead of three services downstream.
Property-based testing. You state a law the code must obey and a generator produces adversarial inputs until it finds a counterexample, then shrinks it to something a human can read. Hypothesis in Python, QuickCheck in Haskell and Erlang, proptest in Rust, fast-check in TypeScript, jqwik in Java.
Deterministic simulation. Run the whole system, or a meaningful slice of it, inside a single-threaded scheduler with a seeded random number generator, a fake clock, and injected faults. Every run is reproducible from its seed. This is how FoundationDB was built, and its influence runs through a generation of storage systems since.
Model checking a design. Write the protocol, not the code, in a specification language and let a checker explore the reachable state space exhaustively within some bound. TLA+ with TLC or Apalache, Alloy, the P language.
Bounded model checking of real code. Compile the actual source into a logical formula and hand it to an SMT solver, which either proves the assertion holds up to a fixed unrolling depth or hands you a concrete counterexample. CBMC for C, Kani for Rust.
Deductive verification of a module. Annotate the code with specifications and discharge the resulting proof obligations, mostly automatically. Dafny, SPARK Ada, Frama-C, Verus, Liquid Haskell.
Full functional correctness. A machine-checked proof, in Rocq or Isabelle or Lean, that an implementation refines a mathematical specification. This is where the decade goes.
What has actually shipped
The useful evidence is not academic. It is the published record of companies that had a hard correctness problem and wrote down what they did about it.
The reference case is Amazon's account in Communications of the ACM in 2015, written by the engineers rather than by researchers. They applied TLA+ to production systems and reported design defects that review and testing had not surfaced, including a data-loss condition in DynamoDB requiring a specific interleaving thirty-five steps deep. Nobody finds that with a unit test. The second finding is quoted less and deserves more: the specs gave the team enough confidence in the design to attempt optimizations they would otherwise have been too nervous to ship. Verification bought speed, not only safety.
The S3 team published a follow-on at SOSP in 2021 on validating a key-value storage node using what they called lightweight formal methods. Rather than proving the implementation correct, they wrote executable reference models of each component, generated operations against both the model and the real code, compared results, and wired it into continuous integration so it kept running after the paper was written. The published account reports sixteen bugs, several in crash consistency, which is the class that survives ordinary testing and surfaces during an incident.
Elsewhere in the same organization: the s2n TLS library carries proofs of its HMAC implementation and record-handling state machine that re-run on every commit. The Cedar authorization language was specified and proved in Dafny, then differentially tested against the production Rust engine so proof and shipping code cannot drift apart silently. Zelkova, the SMT engine behind IAM Access Analyzer and the S3 public-access checks, answers what inspection cannot: can this policy ever permit that access, over all possible requests.
Outside one company the pattern repeats. MongoDB has published TLA+ specifications of its replication protocol, Elasticsearch modeled its cluster coordination layer before rewriting it, and Azure Cosmos DB used TLA+ on its consistency guarantees. Further up the ladder, the CompCert C compiler, verified in Rocq, was the one compiler in a well-known randomized-testing study where researchers found no wrong-code bugs in the verified middle end while finding them in every unverified compiler they tried.
Read that list again and notice what is missing. Not one of these is a proof of a whole system. Every single one is a narrow, deliberately chosen target where the cost of being wrong was high and the state space was too large to test.
Assurance Returned Per Engineer-Week — Our Weighting
Our planning weights for a typical commercial backend. A system where a single defect is unrecoverable moves the bottom two rows up sharply.
Three problem shapes where it pays
Verification is not a quality strategy. It is a narrow blade, worth sharpening on three kinds of problem.
Concurrency and distributed protocols. The defining property is that the bug lives in an interleaving rather than in a line of code. Every component is individually correct and the composition loses data on the ordering nobody imagined. Test suites sample that space at random and the interesting regions are vanishingly small, which is why a lease-renewal or membership-change bug reaches production, sits quietly for eight months, then fires during a partition at the worst hour. A state-space explorer does not sample. It enumerates within a bound you choose and reports the shortest path to the violation.
Authorization, policy and configuration. These look like ordinary code and are secretly logic problems over a small, decidable domain. "Can any request satisfy this rule set and reach that resource" is a question an SMT solver answers exhaustively in milliseconds and a human answers by squinting. Once a permission model, routing table or feature-flag matrix outgrows what one person can hold in their head, a solver is the right instrument and a code review is not.
Parsers, serializers and data boundaries. Round-trip properties are the easiest genuine theorem in software: decode of encode is identity, and two implementations of one format agree. Property-based and differential testing between an old and new implementation catch a large share of real defects here for almost no setup cost, and coverage-guided fuzzing extends it. Open-source fuzzing services running this style continuously have found tens of thousands of bugs across more than a thousand projects, which says a lot about where defects live.
A fourth shape deserves its own line: any state machine where an error accumulates instead of resetting. Ledgers, billing, inventory, anything under PCI scope. A lost or duplicated event causes no outage. It causes a number that is quietly wrong forever, and finding it later is not an engineering cost.
| Problem shape | How it shows up | Technique that fits | Time to first result |
|---|---|---|---|
| Replication, consensus, leases, membership | Rare data loss or split brain during failover, never reproduced | TLA+ or P model of the protocol; deterministic simulation of the implementation | 2–4 weeks |
| Authorization and policy | A permission combination nobody predicted grants access | SMT encoding of the policy semantics; exhaustive query over all requests | 1–2 weeks |
| Parsers, wire formats, migrations | Malformed input crashes a worker; two services disagree on a field | Property-based round-trip tests, differential testing, coverage-guided fuzzing | 2–5 days |
| Ledgers and stateful accounting | Balances drift; reconciliation finds a gap nobody can explain | Executable reference model plus randomized operation sequences compared against it | 1–3 weeks |
| Caches and derived state | Stale reads that only appear under a specific eviction order | Model the invalidation protocol; simulate with a fake clock and injected reorderings | 1–2 weeks |
Where it does not pay, and saying so early
The fastest way to discredit formal methods inside a company is to aim them at the wrong target and burn a quarter. Four targets are reliably wrong.
Anything whose specification is the thing in dispute. Verification proves that code satisfies a statement. If the argument in the room is about what the product should do, a proof adds ceremony to an unresolved disagreement. Business rules that change with the quarter belong in tests that are cheap to rewrite.
User interfaces. The properties that matter are perceptual. There is real work on model-checking interaction flows, and we have never seen it repay its cost against a designer with a prototype.
Model behavior in a machine learning system. You can verify the pipeline around a model: feature computation, the serving path, fallback logic, invariants on inputs and outputs. You cannot verify that the model's judgment is correct, because there is no specification of correct judgment to prove against. Proving that a network's output stays stable under small input perturbations is a real research area and does not scale to deployed models. Evaluation is the instrument there, and it is a different discipline.
Performance. A proof says nothing about latency, and nothing on this ladder will tell you what your tail looks like under load.
The specification is the deliverable
The finding in every honest industrial account, and the hardest one to sell internally, is that the model checker is not where most bugs are found. They are found while writing the model. A prose design document can hide an ambiguity for years, because English lets you write "the leader then updates the followers" without saying what happens if the leader dies between two followers. A specification cannot. Every state, transition and enabling condition has to be named, and naming them surfaces the case nobody considered.
The practical consequence: a team that writes a careful specification and never runs a checker on it has already captured much of the value. The specification is a deliverable in its own right. It outlives its author, survives a rewrite, and gives a new engineer a description precise enough to argue with. Hand a team a two-hundred-line model of a system they have run for three years and the usual reaction is that it is the first unambiguous document about it.
Keep the spec small. A model that mirrors the implementation is worthless, because it will be as wrong as the implementation and harder to read. It exists to abstract away everything except the mechanism you are worried about. If the concern is a lease-renewal race, the model has leases, clocks and failures in it and nothing about storage engines or client retries. Good models are surprisingly short.
Send it over and we will tell you what we would change.
Email the protocol you cannot reproduce a failure in — the design note, or the two or three source files that own the leases, the replication or the state machine — along with the one sentence describing what it must never do, to contact@precisionfederal.com. You get back a short written note naming the three things we would change and why. One business day. No charge, no meeting, no deck.
contact@precisionfederal.comThe cost, honestly
Two numbers anchor the top of the ladder. The seL4 functional correctness proof covers under ten thousand lines of C with roughly twenty times that much proof script, at an effort measured in person-decades. CompCert, verified over a similar span, is a compiler for a subset of C. If someone proposes a proof of your microservice, those are the reference points.
The rungs people actually use cost far less. Our planning figures: a TLA+ model of one protocol runs two hundred to six hundred lines and takes one to three engineer-weeks including the learning curve, most of it spent deciding what to leave out. Property-based tests around a pure core are a day or two for the first useful law. A bounded model check of one function is hours of solver time and a day of harness work, with the cost entirely in choosing the bound. Deductive verification of a module in Dafny or SPARK runs weeks to months depending on how much code must change to become provable, and that clause is where estimates go wrong.
Deterministic simulation is the one whose cost is systematically underestimated, because it is an architecture decision wearing a testing costume. Every source of nondeterminism has to sit behind an interface you control: no direct clock reads, no ambient thread spawning, no unmediated network or disk, no unseeded randomness. Built in from the first commit it is nearly free. Retrofitted into a service that has been growing for four years it is a multi-month refactor that touches everything. This is the rung where early and late differ by an order of magnitude.
Retrofit Difficulty on an Existing Codebase — Higher Is Harder
The two rows at the top are cheap at design time and expensive afterward. That asymmetry is the whole argument for deciding early.
Seven ways a green check lies to you
Every technique here has a failure mode where it reports success and the property does not hold. Knowing them is the difference between using verification and being reassured by it.
- The model is not the code. A verified TLA+ specification says the design is sound. It says nothing about whether the implementation follows the design, and the implementation is what runs. Close the gap with conformance checking, a reference model in the test suite, or simulation traces compared against the spec.
- The bound is the guarantee. Bounded model checking to depth eight proves nothing at depth nine. Exhaustive exploration of a three-node cluster proves nothing about five nodes. Write the bound in a comment next to the check and treat it as part of the claim.
- Every assumption is an unchecked axiom. An assume statement that silently excludes the input that breaks you produces a proof of nothing. Assumptions deserve more review attention than the properties do, and almost never get it.
- The environment is idealized. Real networks deliver duplicates you did not model, reorder across paths you treated as one, and partition asymmetrically so A reaches B while B cannot reach A. If the model omits that, so does the guarantee.
- Timeouts read as passes. A solver that gives up looks like a solver that succeeded unless the pipeline distinguishes them. Every unknown result must fail the build. This is the single most common wiring defect we find in verification setups that have been running for a while.
- A verified part in an unverified whole. Proving one component correct moves the defect to the interface, where the value crossing the boundary, the error path and the units now decide the incident.
- The specification drifts. The protocol changes, nobody updates the model, and the checker keeps passing on a description of a system that no longer exists. This is worse than having no specification, because it carries authority.
If it is not in the build, it is a paper
Verification artifacts rot faster than code because nothing breaks when they go stale. The correction is mechanical, and it is why the s2n approach of re-running proofs on every commit matters more than the proofs themselves. Put the specification in the same repository as the implementation. Run the checker in the build on a bounded configuration sized to finish in a few minutes, and the expensive configuration nightly. Fail on a violation and on an inconclusive result equally.
Then the social half, which tooling cannot do. A pull request that changes the protocol and not the model is a review comment, not a merge. Someone owns each specification by name. When an incident traces to a protocol defect, the first review question is whether the model could have caught it, and if so, why it did not.
Property-based tests need their own discipline: save every failing seed as a permanent regression case, run a fixed seed set on every commit, and run fresh seeds nightly so the suite keeps searching. A property suite that never finds anything new has usually stopped generating anything new.
A thirty-day way to start
You do not adopt formal methods. You aim one technique at one problem, and it either returns something in a month or it does not.
First Thirty Days
Thirty days is enough because every expensive unknown here is measurable inside it. Whether your team can write a specification is answered by having them write a small one. Whether your architecture can be simulated deterministically is answered by seeding one component. Whether your properties are statable at all is answered on day three, and if they are not, that is the finding, and it is worth more than the tool selection you were about to do instead.
Choosing a tool, briefly
Tool choice matters less than people expect, and it matters at the margin. The short version of a landscape that changes slowly.
| Tool | What it checks | Fits | Watch out for |
|---|---|---|---|
| TLA+ with TLC or Apalache | A design, exhaustively within a finite configuration | Replication, consensus, leases, cache coherence, workflow state machines | State explosion; the syntax costs a week of morale before it starts paying |
| P | Event-driven state machines, with a programming-language feel | Teams that want a model closer to how they already think about actors and messages | Smaller community and fewer worked examples than TLA+ |
| Alloy | Structural and relational properties within a bounded scope | Data models, permission graphs, schema and ontology questions | Bounded scope only; excellent for finding counterexamples, weak for proving absence |
| CBMC and Kani | Real C or Rust, up to an unrolling bound | Individual functions where memory safety or arithmetic edges matter | Harness quality decides the result; loop bounds quietly cap coverage |
| Dafny, SPARK, Verus | Code against annotations, discharged mostly automatically | A small component whose correctness is worth months and whose interface is stable | Code often has to be restructured to be provable; that cost is the estimate |
| Z3 and CVC5 directly | Whatever you encode into logic yourself | Policy, configuration, scheduling and allocation questions | Encoding is the engineering; a wrong encoding proves the wrong theorem |
| Hypothesis, proptest, fast-check | Laws about your code, tested against generated adversarial inputs | Everywhere, starting today | Weak generators produce a suite that passes and covers nothing |
Own these regardless of how far up the ladder you go
- A written list of invariants the system must never violate, in the repository
- A pure core with input, output and clock access pushed to the edges
- A seeded deterministic test mode, even if only one subsystem supports it
- An executable reference model for every stateful component, however crude
- Saved failing seeds as permanent regression cases, with the shrunk input
- The bound written next to every bounded check, and inconclusive results failing the build
- A named owner per specification, and a rule that a protocol change without a model change does not merge
Bottom line
Formal verification outside academia is not a research program you adopt. It is a ladder, and the bottom four rungs are ordinary engineering that pays for itself within a month on the right problem. Aim it at concurrency, at policy, and at data boundaries, where the state space defeats testing and the cost of being wrong is a number that stays wrong. Write the specification for the thinking it forces, keep it small, put it in the build so it cannot rot, and record the bound so nobody mistakes a partial claim for a total one. Leave the top of the ladder to the people building compilers and kernels, where it has already earned its keep.
Frequently asked questions
The lower rungs are. Property-based testing, executable reference models and deterministic simulation are ordinary engineering practices that a team can adopt in weeks. Model checking a protocol design takes one to three engineer-weeks for the first model. Machine-checked functional correctness proofs are a different category and are almost never the right call for application software.
Model checking explores a state space automatically and either finds a counterexample or exhausts the space within a bound you set. Theorem proving builds an argument that a property holds in all cases, with a human guiding the proof and a machine checking each step. Model checking is far cheaper and gives a bounded guarantee; proving is far more expensive and gives an unbounded one.
No, and this is the limitation to state out loud. A verified specification establishes that the design is sound; the implementation can still diverge from it. Narrow the gap with conformance testing, an executable reference model compared against the real code on random operation sequences, or simulation traces checked against the specification.
You can verify the system around the model: input validation, feature computation, the serving path, fallback behavior, and invariants on outputs. You cannot verify that the model's judgment is correct, because there is no specification of correct judgment to prove against. Proving output stability under small input perturbations is an active research area and does not scale to production-sized models. Use evaluation for model quality and verification for the plumbing.
Write down the three outcomes your system must never produce, add property-based tests for the laws behind them around whatever pure code you have, and wire those into continuous integration with saved failing seeds. If a protocol has already caused a production incident, model that protocol and nothing else. Thirty days is enough to know whether the approach fits.