Runtime Verification
← All posts

The proof is in the spec

Posted on September 30th, 2026 by Palina Tolmach, Natalie Klaus
Last updated on September 30th, 2026
Posted in News

the-proof-is-in-the-spec.png

Boris Cherny, who leads Claude Code at Anthropic, posted recently that he pointed Opus 5.5 at the Claude Agent SDK, had it formalize the code in Lean (and sometimes TLA+), and got 16 PRs fixing bugs and race conditions out of a couple of short prompts.

The bugs are real and the result is genuinely good news. AI plus formal methods is an excellent bug-finding workflow because formalization forces both a human and a model to explicitly reason about behavior and assumptions. AI is also changing what's worth attempting with formal verification: with AI doing much of the proof work, we're now aiming at targets that would have been out of reach a few years ago. With AI, formal models are also becoming more economically valuable even before full verification: once built, they can serve as executable references for fuzzing, regression testing, and code generation, not just as inputs to proofs.

But it's worth being precise about what a fully LLM-driven run like this actually establishes. It can find bugs very effectively, but it doesn't yet answer "is this code correct?". As proof construction gets cheaper, the bottleneck has moved to specification, modeling, and choosing the right abstractions, assumptions, and formalisms.

The backlash is half right

The replies to the tweet split fast. Some readers took the post as proof that verification is now a prompt away. Others said everyone is larping, nobody knows what these proofs even verify, and there's no "prove there are no bugs" magic wand.

Much of the skepticism isn't about formal verification itself but about vibe-formalization: proofs about models nobody checked, against specifications nobody reviewed. That's a fair concern. A proof that type-checks establishes that a theorem follows from a particular formal model and set of assumptions. It does not, by itself, establish that the model faithfully represents the implementation or that the theorem captures what the program was actually supposed to do. Without a trusted foundation, such as a formal semantics or a validated translation pipeline, AI is unlikely to get those right on its own, as demonstrated in the academic work listed in references.

Those are engineering problems, not proof-search problems. Take a concurrent queue. Before proving anything, you have to decide: is the property memory safety, linearizability, lock freedom, FIFO ordering? What memory model do we assume? Can allocation fail? Can callbacks re-enter? Which operations are atomic? A prover can establish a theorem only after those choices are made, and a valid proof of the wrong property is still the wrong result.

Getting formal verification guarantees for such components is challenging but feasible. seL4, a microkernel of about 8,700 lines of C, has a machine-checked proof of functional correctness: the code does exactly what its specification says, for every input. It's one of many such results, from verified compilers to the cryptography running in the Linux kernel. It took years of expert work on specification before a single proof mattered. That's the point.

Where the gap is

A machine-checked proof tells you one thing: this theorem follows from these definitions and axioms. Whether that means anything for your code depends on two questions the checker can't answer. Does the model accurately represent the implementation? And does the specification say what we actually want? When an LLM writes the model, the spec and the proof, and nobody reviews the first two, both can go quietly wrong.

The model is not the code. If Claude reads TypeScript and writes Lean or TLA+, the result is Claude's interpretation of the implementation. It can drop an error path or assume a callback never re-enters, and the proofs won't notice. That may still be useful for finding bugs, but a proof about that model is not automatically a proof about the program. The missing piece is a justified connection between the two.

For implementation-level verification, we generally want this connection to be mechanical: extraction or translation based on a defined semantics of the source language, ideally with the translator itself verified or independently validated. Proving a translator correct is a large project, but a well-understood one: show that each construct translates correctly and lift that to whole programs by induction on their structure, as CompCert famously did for a C compiler. An LLM translator gives you no comparable guarantee. Mechanical translation also fails differently: when you find a bug in a translation rule, you can fix the whole class of translations systematically rather than correcting a single LLM-generated output. A lighter-weight check that works for any executable model is differential fuzzing: compile the model to a binary, run it and the original program on the same generated inputs, and compare the results. It doesn't prove equivalence between the program and the model, but it catches some translation bugs cheaply, and with a mechanical translator every bug it finds is fixed for good.

For a protocol or concurrent design, a deliberately abstract hand-written model may be the right level instead. Then the obligation is a refinement or conformance argument showing that the implementation's relevant behaviors are represented by the model. That argument is exactly the step autoformalization tends to skip.

Benchmarks show this happening. The SysMoBench team asked Claude for a TLA+ spec of Etcd's Raft implementation and got back what was essentially the spec from the Raft paper's appendix: it passed every check and had little to do with Etcd. In a ZooKeeper spec, the model stored received votes as a set, keeping stale votes around, where the real code uses a map that overwrites them. Across frontier models, specs scored near 100% on syntax but around 46% on conformance to the actual code.

The spec is not the intent. A theorem can be true and useless: weak postconditions, hypotheses nothing satisfies, invariants that hold because the interesting state is never reached. An agent rewarded for making the proof go through has an incentive to weaken the statement rather than find the bug.

Here's what that looks like, in an example from the FaithformBench paper (Cornish et al., 2026). Given the deliberately wrong step "3^x = 5, so 3^(x+2) = 51" (the right answer is 45), the Kimina autoformalizer produced:

theorem step (x : ℕ) (h : 3^x = 5) : 3^(x+2) = 51

It quietly made x a natural number. No natural number satisfies 3^x = 5, so the hypothesis is impossible and the false claim becomes provable. The FaithformBench authors found this kind of silent correction across all fine-tuned formalizers they tested, and worst in the ones that were best at formalizing correct statements. Other studies agree: an agent that got 89.5% of graduate-level Lean statements to compile produced faithful ones only 60.5% of the time, and in Verus, LLM-written specs omitted input assumptions, accepted wrong outputs and rejected correct ones, with LLM judges missing a quarter of those failures.

Autoformalization makes the model and specification much cheaper to produce, and makes them much easier to skip reviewing.

How we do it with maintainers

When a maintainer comes to us with critical code, the work goes through five stages. Each stage produces an artifact that gets checked, by the maintainer or by the proof checker.

the-proof-is-in-the-spec-image-1.png

  1. A specification in plain English. Before any Lean, we write down what the code is supposed to do: inputs, outputs, error cases, invariants, concurrency assumptions, what happens on malformed data. It has to be exhaustive, and it's written for the maintainer, not for a prover. The maintainer reviews it and tells us where we're wrong. This is the stage that answers "what does it even verify?".

    For the queue, for example, this is where the maintainer confirms that the target is linearizability under the kernel memory model, and that a failed allocation must return an error without losing any queued item.

  2. A mathematical model of the code. How we build it depends on the language, the size of the code, its complexity and what the maintainer needs. For Rust we extract Lean mechanically through Charon and Aeneas. For C we use our own translator into Lean, whose C semantics is executable, so we can fuzz the model against the original code. For a protocol or a concurrent design, a hand-written abstract model may be the right level, with a refinement argument linking it to the implementation. Where a translator is involved, it's something we have to trust, so it gets tested like any other software. We've found and reported bugs in extraction tools ourselves.

  3. The specification, formalized. We turn the English spec into theorems, or another formal statement where theorems aren't the natural fit. Each formal statement traces back to a sentence the maintainer already approved. We check the statements for vacuity: mutate the implementation and make sure the proof breaks, try to derive False from the hypotheses, list the axioms each result depends on.

    For the queue, for example, the theorem states that every concurrent execution is equivalent to some sequential FIFO execution that respects the real-time order of operations.

  4. A proof that the code meets the specification. This is where AI earns its keep. We use AI provers heavily here, because a bad proof can't get past the checker. Failed proofs are often the most valuable output of the whole project: each one is either a bug in the code or a gap in the spec, and both go back to the maintainer.

  5. Functional correctness, as the goal. Functional correctness means that for every valid input the code produces exactly the result the specification describes (and, where it matters, that it terminates). That's a stronger claim than "doesn't crash" or "no out-of-bounds access": the code computes the right thing, always. Stage 4 can prove a subset of properties, say memory safety plus the invariants the maintainer cares most about. Stage 5 is reached when the spec is complete and the proof covers all of it. It's hard, and not always reachable with today's tools and techniques. It's what we aim for, and when we fall short, we say exactly which properties were proved and which weren't.

    For the queue, stopping at stage 4 might mean proving memory safety and no lost items, while stage 5 adds that the queue is linearizable and FIFO in every execution.

Every result we ship states what was verified, against which spec, under which assumptions, and what sits outside: the runtime, the allocator, unverified parsers, the hardware.

The short version

Let AI write the proofs. Don't let it decide, unchecked, what they prove. Verification starts with a specification a maintainer agrees with and ends, when it goes all the way, with functional correctness. Everything in between is engineering, and it's where most of the value is.

References