Nothing Checks the Spec

Andrew Helwer published a post on August 24 that reads like a career obituary and is actually a map. He works in formal methods — TLA+, model checking, the discipline of proving that software does what you claimed it does. He is watching his corner of it go obsolete for the second time.

The first obsolescence was around 1995. Finite-state model checking — literally: enumerate every reachable state of your system, check your invariant at each one — got outclassed by symbolic methods that could handle state spaces too large to walk. Helwer says it flatly: technically obsolete since the mid-nineties. Last year he went to ETAPS 2025, the field's main academic conference, and did not see a single talk on the subject.

It survived anyway. Thirty years past its own funeral. It survived for one reason, and that reason is the whole story.

i · it survived because you can read it

Helwer's line: "Any software engineer of any education can understand breadth-first search."

That's the entire moat. Finite-state model checking is worse by every technical measure and it persisted for three decades because a working engineer can hold the whole algorithm in one head. The symbolic methods that replaced it are far more powerful and exhibit what he calls performance cliffs — they work brilliantly until they don't, for reasons that take graduate training to diagnose. His summary is careful: "There is simply value in using tools that you understand, which may or may not outweigh the value given by the power of incomprehensible tools."

Note the hedge on the end. He isn't a purist. He's naming a trade with real weight on both sides.

The second obsolescence is AI, and it's economic rather than technical. The old calculus was an 80/20 bargain: a large amount of effort to formally prove your system properties correct with full confidence, or twenty percent of that effort to model-check it and get perhaps eighty percent of that confidence. A whole profession lived in that middle. Automated theorem proving has gotten good enough to collapse the cost of the expensive option, and when the expensive option gets cheap, the middle stops making sense.

Which brings us to the sentence I keep turning over. On AI-generated proofs being unreadable by any human: "Assuming you trust your proof system the incomprehensibility is not such a drawback, but anyway."

He's right, trailing shrug and all. If the proof kernel is sound, an unreadable proof is exactly as good as a readable one. That's what a proof is. But look carefully at what just happened to the position of the human.

ii · verification is comprehension relocated

Here's what the conversation about AI and verification keeps getting wrong.

We talk about verification as though it replaces comprehension — as though the tool understands the system so you don't have to. It doesn't. Every verification tool moves your comprehension somewhere else and demands it just as fiercely at the new address.

When you model-check, you don't read the state space; you read the invariant. When you accept a machine proof, you don't read the proof; you trust the kernel. When you write a specification and let a model generate the implementation, you don't read the code; you read the spec.

That middle one deserves a moment. Helwer links, almost in passing, to a postmortem for kernel soundness bug 14576 — published three weeks before his own post. Not a thought experiment. A filed, diagnosed, written-up defect in the one component whose correctness everything downstream is resting on. You trust the kernel precisely because you can't check the proof yourself, and the kernel is software, written by people, on a deadline. Trusting it is a bet. It is usually an excellent bet. Someone has already collected on the other side of it.

Every one of those relocations is still a good trade. The artifact you become responsible for is smaller and denser than the one you handed over. A twenty-line invariant instead of forty thousand lines of implementation is enormous leverage, and refusing it on principle is just expensive pride.

But notice the direction. Each step moves human judgment upward, toward artifacts that are smaller, more abstract, and more load-bearing. And at every step, the artifact you're now holding is the only place your judgment enters the system at all.

That's fine. That's good. Right up until you stop moving with it.

iii · nothing checks the spec

The failure mode isn't "AI writes bad code." Verification handles that, and handles it better than you do. The failure mode is much quieter.

A model checker will prove your system never violates the three invariants you wrote. It will do this perfectly, exhaustively, with a rigor no human code review can approach. It has nothing whatsoever to say about the fourth invariant — the one you didn't think of, the one describing the failure that actually takes you down at 4 a.m. on a holiday weekend.

Specs are silent about what you forgot to say. And there is no tool downstream of the spec that catches what's missing from the spec, because downstream is defined relative to the spec. Verification proves conformance. It cannot prove that conformance was the right thing to want.

So the guarantee you actually hold, stated honestly, is this: this system does not fail in the ways I was able to imagine. That's a real guarantee. It's worth a great deal. It is also dramatically narrower than "this system is correct," and the gap between those two sentences is where every interesting outage lives.

When the implementation goes opaque — when nobody on the team has read the generated code and nobody reasonably could — the spec stops being a document about the system. It becomes the entire surface of your relationship to it. Every judgment you hold about that software now lives in one artifact. Nothing else you own touches it.

That's the trap. And the trap isn't trusting the tools. It's failing to notice that the room your judgment used to live in is now empty, and standing guard there anyway. Reviewing pull requests line by line with great care, while the load-bearing decision was made three levels up, in a spec that got a fraction of that attention because it was only a page long.

iv · move with it

Four things. You can do the first one tomorrow, before you open an editor.

1. Write the invariants before you write the prompt. Before you ask a model for an implementation, write down what must never happen. Not what it should do — what must never be true. That list is a values question wearing engineering clothes, and it is the one artifact no tool can generate for you, because the tool doesn't know what you can afford to lose.

2. Move your review ritual to where your judgment went. Whatever discipline you had around code — a second reader, a checklist, sleeping on it before merging — relocate it. The artifact carrying your judgment is the artifact that earns your review process. If your spec gets a skim and your generated code gets an hour, you have the ritual pointed at the wrong artifact.

3. Write down the boundary of your guarantee. A green verification run tells you about the failures you named. Keep the complement in the same file as the spec: concurrency you didn't model, failure modes you scoped out, assumptions about the environment you never tested. Then do the same in the other direction — for every guarantee you're leaning on from someone else, the kernel, the vendor, the model, write down what would prove it wrong. None of this is a confession of sloppiness. It's what stops a guarantee from quietly inflating in everyone's memory between now and the incident review. A guarantee with no conceivable falsifier isn't a guarantee. It's a mood.

4. Keep one comprehensible link in the chain. This is Helwer's breadth-first-search point, generalized. If every link in your trust chain is opaque — generated code, verified by a prover you can't read, on a kernel you take on faith, running on silicon you've never audited — you don't have verification. You have faith with better tooling. Keep one tool in the chain you could rebuild from scratch, or one check you could run by hand on a small case. It doesn't have to be the strongest link. It has to be the one you'd actually stake something on.

v · the room where judgment lives

You cannot govern what you cannot read — that's the commitment underneath all of this. But the honest version of it in 2026 is not "read everything." You can't, and pretending otherwise is a way of losing slowly. The honest version is narrower and harder: know where the last human judgment enters your system, and stand there.

That location moves. It moved from machine code to source, from source to specification, and it will move again. Every move is a genuine gift: a smaller artifact, more leverage, less to carry. Take them. Take all of them. But follow. Agency doesn't die when a tool becomes more powerful than you are. It dies when the point where you mattered relocates and you don't relocate with it — when you keep guarding a room that nothing passes through anymore.

Helwer ends by naming where his own attention goes next — a split between formal proofs and a fleshed-out story for deterministic simulation testing. He isn't mourning the room he's leaving. He's relocating, in public, on the record. That's the part worth copying, rather than his particular answer. The tools will keep getting better at the part you used to do by hand. What stays yours is deciding what to want, and writing it down clearly enough that a machine can check it.

Nothing checks that. Someone has to.