Generated by Codex with GPT 5.6 Sol XHigh

The Pragmatic Engineer surfaced the piece in “Formal methods with Hillel Wayne”, a conversation about a question made more urgent by AI-generated code: if software can be produced faster than people can understand it, what should teams trust as evidence that it is correct?

Wayne’s answer is deliberately unspectacular. Formal verification will become more useful, but it will not become the default for ordinary software. Most teams would gain more from stronger testing habits, especially property-based testing. Formal methods earn their cost when a system is complex, concurrent, safety-critical, or expensive enough that testing individual examples cannot give sufficient confidence.

Debugging the design

Conventional tests run one implementation against a chosen set of examples. Formal methods can work at a different level: they describe a system precisely, state the properties it must preserve, and let a tool explore the states or execution paths allowed by that description.

TLA+, the specification language at the center of the episode, models a system as states and transitions between them. Engineers define safety properties—things that must never happen—and liveness properties—things that must eventually happen. A model checker can then search possible event orderings for a counterexample. This is particularly useful in distributed systems, where message delays, retries, crashes, recoveries, and concurrent operations create combinations that are difficult to reproduce or even imagine.

The episode’s strongest example comes from AWS. In its paper “Use of Formal Methods at Amazon Web Services”, the company described a DynamoDB design flaw whose shortest failing trace required 35 high-level steps. The bug had survived extensive design review, code review, stress testing, and fault-injection testing. TLA+ found it because the model checker could systematically explore interleavings that human reviewers were unlikely to enumerate.

That does not mean the tool proved every line of DynamoDB correct. A formal model is an abstraction, and it only checks the properties its authors chose to express. Its practical value was narrower and more important: it exposed a serious error in the design before that error could damage customer data.

Use the lightest tool that buys enough confidence

If formal verification can find bugs that tests miss, why not apply it everywhere? Because writing the specification is itself difficult work. Even a request as simple as “find the file with the most lines” immediately raises questions about encodings, unreadable files, symbolic links, and what counts as a line. Most software does not justify resolving every edge case with mathematical precision.

Wayne therefore recommends a ladder of assurance rather than an all-or-nothing choice. Unit and integration tests remain useful for known examples. Property-based tests go further by stating an invariant and generating many inputs that try to break it. Formal specifications and model checking belong higher on the ladder, reserved for systems whose state space, concurrency, or failure cost warrants the extra effort.

This framing makes property-based testing the episode’s most broadly useful recommendation. It asks engineers to move from “does this example return the expected answer?” to “what must remain true across a large range of inputs?” That shift captures part of the discipline of formal methods without requiring a separate model of the entire system.

Formal techniques become attractive when failures emerge from sequences rather than isolated inputs. Time-of-check-to-time-of-use bugs are a good example: a program verifies a condition, time passes, and the condition changes before the program acts. The check can be locally correct while the overall operation remains unsafe. Modeling the state transition makes the hidden assumption visible.

AI lowers friction, not the need for judgment

The fashionable prediction is that AI-written software will make machine-checked specifications universal. Wayne expects a smaller change: AI may expand formal verification from a tiny niche to a somewhat larger niche, which would still be meaningful.

LLMs can explain unfamiliar syntax, draft a model, and help experienced practitioners work faster. But they do not remove the hardest part—deciding what the specification should guarantee. In “LLMs are bad at vibing specifications”, Wayne shows AI-generated examples that either fail to run or verify weak, nearly tautological properties. A model checker reporting success is not useful if the model never asked a consequential question.

This is the same verification bottleneck appearing twice. AI can generate code that looks plausible but is wrong, and it can generate a specification that looks rigorous but proves very little. In both cases, the scarce resource is an engineer who understands the system well enough to identify strong properties, meaningful abstractions, and dangerous omissions.

The most durable takeaway is not that every team should adopt TLA+. It is that reliability begins by making assumptions explicit. Teams should define what must never fail, use property-based testing where examples are too narrow, and reach for formal models when concurrency or consequence makes ordinary testing inadequate. AI can accelerate each layer, but it cannot decide which truths matter.