The proof passes. Of what?

Boris Cherny, Creator and Head of Claude Code at Anthropic, posted on 23 September that he'd used Opus 5.5 to formally verify the Claude Agent SDK using Lean. His words: "A couple short prompts = 16 PRs fixing various bugs and race conditions." TLA+ works well too, he said, and he sometimes combines the two to look at data flow, concurrency and state. Then the admission I liked most: "I don't know either language well, but Claude is excellent at both." And the question he left the thread with: "Is formal verification the future of coding (or at least, bug finding)?"

Sixteen real fixes, race conditions among them, from a technique most teams have filed under "for compiler people". That is great news, whatever else follows. If the model has made formal methods cheap enough that a busy engineer reaches for them on a Tuesday, that's a gate a lot of us have wanted for years and never had the budget for.

The best question in the thread came from Mustapha Derzi, VP of Application Development at OtisEd with thirty-plus years of enterprise architecture behind him. When Claude writes both the Lean model and the proof, he asked, what catches the case where the model diverges from what the code actually does, so the bug lives in the gap between them? Nobody answered it well. I'd like a go, because the honest answer is bigger than the question.

Four things hiding in one sentence

For anyone who hasn't met the tools. Lean is a proof assistant that is also a programming language: you state a property, you write a proof that it holds, and the machine checks every step, with no room for "looks fine to me". TLA+ is a language for writing down how a concurrent or distributed system is meant to behave, so the design can be checked above the code. Formal verification, in the sense Boris means, is building a mathematical model of your code and proving properties about it, rather than running tests and hoping you thought of the cases that matter.

So when someone says "the proof passes", there are four things in the sentence and only one of them is the proof. There's the code. There's the model of the code, which is what the proof is actually about. There's the property, the statement of what must be true. And there's the requirement behind the property, the plain-English reason anyone cared. A passing proof tells you the model satisfies the property. It says nothing about either end of that line: whether the model is the code, and whether the property is the requirement.

Mustapha's question is about the first gap, and it has a mechanical answer, at least in part. Tools like Aeneas derive the Lean model from the Rust source instead of having it written, so for the subset of safe Rust it handles there's no gap for the bug to live in. The SDK Boris verified isn't Rust as far as his post says, so I'm pointing at the kind of fix, not claiming it applies to his run. Model-versus-code is a gap that machinery closes.

The second gap isn't.

No prover can tell you the property was the right one

The projects that have done this properly say so themselves. seL4 is about as thoroughly verified as an operating system kernel gets, and its own FAQ, asked whether it has zero bugs, answers yes "in the understanding of formal software verification (code implements specification)", then adds that "there may still be unexpected features in the specification" and that its security properties "may be sufficient for what your system needs, but might not". Hillel Wayne's example is the one I'd hand an exec: a proof that leftpad returns a string of length max(n, len(s)) is a proof about a length. What the user wanted was text that lines up on the screen. The proof passes. Of what?

That's the gap Boris's demo doesn't touch, and to be fair to him, his post never claimed it did. It's bug finding at the code layer, and it's clearly good at it. But somebody chose the properties. In any real system, "no two callers hold the lock at once" and "a cancelled request never bills the customer" are both provable, and only one of them is what the business would have written down. Which one depends on who's paying, and no prover has an opinion.

What the proof proves against

Where I've landed after a year of building software this way is a chain with both ends written down. A requirement, in the words of whoever owns the outcome. Under it an acceptance criterion: a short, checkable statement of what the software must do in a specific scenario, written before the build and agreed by a named person, so there's someone to ask when it turns out to be wrong. The property is that criterion made explicit enough for a prover to read. The proof is the check. And the evidence, the thing you put in front of an auditor, is the whole line: this requirement, this criterion, this property, this proof, these dates, these names. I've a longer page on the middle of that, acceptance criteria as the contract, and formal verification slots underneath it without changing a word.

The exec version, once: the method says what must be true, and the prover shows it stays true.

Seen that way, Boris's result and the chain aren't competing for the same job. His is the strongest link I've seen offered for the verify step, and I'd go so far as to say that where a property can be stated in Lean, a passing proof beats any test suite I've ever shipped. It just has to be a proof of the right thing, and "right" is a decision no machine takes for you. Most teams I work with won't be writing Lean this year, and honestly, it's a tool I've never needed to reach for; the chain applies to them anyway, with tests in the slot, and it'll still apply when the proofs arrive.

So next time a demo ends with "the proof passed", and there will be more of them, three questions. Of what? Agreed by whom? Where's the evidence? If those have answers, you've got something an auditor can sign. If they don't, you've got a very expensive test that's certain about something nobody chose.

That's the RCF methodology in one paragraph, the way I've built with agents this last year, and it's put high-stakes, auditable software into production. Formal verification is the best gate I've seen offered for it. I'll take it, gladly. I'd just like to know what it's proving.