A proof can establish that a program satisfies a specification. It cannot establish that we specified the right thing.
That distinction used to sound like a warning for the small group of engineers working with formal methods. It is becoming relevant to the rest of us. Agents can now produce more code than humans can sensibly inspect, while an ordinary test suite still samples only part of the behaviour.
The tempting conclusion is that formal verification must replace testing. I think that is the wrong conclusion. The interesting possibility is narrower: agents may reduce enough of the mechanical cost of formalisation that proof becomes practical for more parts of ordinary software. If that happens, proof joins our verification stack. It does not become the stack.
What May Have Changed
Formal verification is expensive for several reasons. We have to describe the relevant semantics, state the property precisely, find a proof, connect the model to executable code and maintain all of it as the system changes. Specialist tools and a limited pool of experienced practitioners add to the cost.
An agent can help with some of that work. It can translate a simple model into a proof assistant, search a library for useful lemmas, react to a failed proof obligation and repeat the dull parts of a refactor. Crucially, the proof checker does not have to trust the agent’s explanation. It checks the resulting proof.
Stephen Diehl’s February 2026 experiment with Claude Opus 4.6 and Lean is a useful illustration. He reports building roughly 900 lines of category theory in two half-hour sessions. The Lean kernel accepted the proofs, but the model still needed guidance on harder steps and produced technically valid proofs that Diehl later simplified for humans. This was a small, self-reported experiment by an expert who already understood both the mathematics and the benchmark. It shows an agent participating in non-trivial formalisation under good conditions; it does not establish the cost of verifying ordinary application code.
The feedback loop matters as much as the model. A proof assistant exposes an exact goal, accepts or rejects the attempted proof and gives the agent another chance. That is a much cleaner signal than asking a second model whether the first model’s code looks correct. More reasoning does not repair an imprecise oracle; a machine-checked obligation at least tells us whether this particular claim follows from the definitions and assumptions provided.
I would therefore treat the changed economics as a hypothesis with encouraging evidence:
Agents can make the search, translation and maintenance around proofs cheaper. Humans still pay for choosing the model, challenging its assumptions and deciding which properties deserve the effort.
We should measure both halves. A quick proof that formalises the wrong contract is not a saving.
What a Proof Actually Covers
The official Lean theorem-proving guide defines formal verification in terms of precise mathematical claims that a system meets its specification. It also explains the value of proof objects that can be checked independently. Both phrases matter: precise claim and its specification.
Suppose we model a replicated log and prove this invariant:
Every acknowledged entry remains present after one node fails.That is a meaningful result, provided the model describes acknowledgement, storage and failure accurately. It does not by itself prove that:
- the disk honours the write semantics assumed by the model;
- the network library maps errors to the states we modelled;
- two nodes cannot fail when the deployment says only one will;
- an operator cannot load an incompatible configuration;
- clients interpret an acknowledgement in the same way;
- the service is fast enough, usable or worth operating.
The proof may cover every state in the mathematical model while production fails just outside its boundary. This is not a defect in proof. It is a reason to publish the boundary with the result.
A useful verification report should say which property was proved, against which model, with which assumptions, and how the model relates to the running implementation. It should also expose admitted axioms, approximations and unmodelled dependencies. A green badge without that information invites readers to interpret “proved” as “correct in every relevant sense”. Software rarely offers such a convenient claim.
The Specification Is Another Program
The specification can contain a bug. In fact, it can contain the most expensive kind of bug: a precise description of the wrong behaviour.
A payment proof may guarantee at-most-once charging while forgetting that a declined payment must never be marked as settled. The mistake can also sit upstream: an authorisation function may match a policy which grants access to the wrong group. Even a correct safety property can omit liveness, leaving a system which never corrupts data because it never completes any work.
An agent can make this worse in a subtle way. If the same prompt produces the implementation, the formal model and the proof, all three may share the same mistaken assumption. Independent proof checking protects the logical steps. It does not provide an independent understanding of the business.
This is why specifications are the interface, not an oracle handed down from elsewhere. They need examples, domain review, counterexamples and revision. For important properties I would want somebody other than the implementation agent to try to falsify the model: find a missing state, relax an assumption, construct an awkward input, or explain a plausible production failure which the theorem does not cover.
Proof moves the argument to a better place. Instead of debating whether a loop looks right, we debate what “right” means. It does not end the argument.
Use the Lightest Check That Can Reject the Error
Different checks answer different questions. Making formal methods cheaper does not make the other questions disappear.
| Mechanism | Good at | Important limit |
|---|---|---|
| Unit and integration tests | Concrete behaviour and fast regression feedback | They cover selected examples and environments |
| Property-based and differential tests | Exploring many inputs and comparing independent implementations | The generator and reference can still miss the real contract |
| Types and static analysis | Ruling out classes of invalid state or unsafe construction | Expressible properties depend on the language and tool |
| Model checking and deterministic simulation | Exploring transitions, faults and concurrency schedules | Searches may be bounded or rely on a simplified model |
| Theorem proving | Establishing a stated property for all cases represented by the model | The specification, assumptions and code-to-model connection remain obligations |
| Staging and production observation | Seeing real dependencies, traffic and operational behaviour | Observation detects outcomes after execution; it cannot enumerate every future case |
Tests remain the better tool when examples are cheap, failures are easy to observe and the behaviour changes frequently. A form validation rule, a rendering detail or an adapter around an unstable third-party API will often gain more from a clear test and a real execution than from a maintained proof model. Exploratory testing is also better when we do not yet know what the correct behaviour should be. Formalising uncertainty does not remove it.
Proof becomes attractive when the property is precise, important and reused: a cryptographic primitive, a parser, a state transition which protects money, a protocol invariant, or a rule that must hold across a huge input space. The longer the component lives and the more other software depends on it, the more chances there are to recover the initial cost.
There is a useful middle ground too. Types can make invalid states unrepresentable. A small reference implementation can act as an executable specification for differential tests. A TLA+ model can explore a protocol before anybody attempts a theorem about the implementation. We do not earn extra points for choosing the most intimidating tool.
A Case Study in Layers
Datadog’s harness-first distributed systems report is interesting precisely because it did not rely on one form of verification. The company reports that agents built a Redis-compatible server and a Kafka-like streaming service while engineers added layers as failures exposed gaps: a shadow-state oracle, deterministic simulation with injected faults, TLA+ specifications, bounded checks with Kani, compatibility suites and staging traffic.
In the Helix project, Datadog says deterministic simulation was the everyday workhorse, while model checking and bounded verification were used where stronger claims justified their cost. Human engineers still chose the invariants and approved consequential architectural decisions. Tests that passed early in the project had not caught compatibility differences or timing-dependent failures; later verification did not make production observation redundant either.
These are first-party results from Datadog, not an independent evaluation or a long production history. The projects also benefited from the company’s experience operating distributed systems and from substantial investment in the surrounding tooling. What I take from the report is not its performance comparison. It is the shape of the method: use several disagreeing mechanisms, and strengthen the cheapest layer that allowed an error through.
That method is less glamorous than “AI proves all its code”. It is also much more believable.
The New Cost Model
Before adopting formal methods, I would ask four questions:
- Which failure are we trying to exclude? “Correctness” is too broad to budget.
- Can we state the property without pretending away the difficult part? If the key behaviour lives in people, external services or changing policy, a proof model may be premature.
- How is the model connected to the executable system? A verified design and an unrelated implementation give us two artefacts, not one guarantee.
- Who will maintain the proof when the contract changes? Generated proof code is still code, and stale proof infrastructure is particularly good at creating false comfort.
Then compare the alternatives. A stronger type, a smaller interface, a reference implementation or better fault injection may remove the same risk for less effort. For a stable and critical component, a maintained proof may be cheaper over its lifetime than repeatedly testing around the same uncertainty.
Agents alter this calculation because they can perform more of the repetitive work and consume precise checker feedback without exhausting a human. They may also increase the need for stronger verification by increasing the volume of implementation. Both effects point in the same direction, but neither makes proof free.
I expect formal verification to move from an exceptional technique towards a practical option for carefully chosen components. I do not expect every application to become a tower of theorems. The useful future is a verified core surrounded by tests, simulations, operational evidence and explicit assumptions.
Proof is mathematical friction. Used well, it slows down the part where we decide what must always be true, then lets generation move quickly inside that boundary. That seems like a fair price. The important bit is remembering who chose the boundary.