The proof is impossible. Refactor. The proof is trivial. (September 2026)

We keep having the same experience: a theorem about our code fights back for hours, we refactor the code, and the same theorem proves in one line. After the seventh time, it stops being an anecdote and starts being a methodology — proof difficulty is a code-quality metric, and an LLM makes it cheap enough to use as one.

Yesterday one of our agents shipped a bug of a particularly modern kind. Our coding agent, l3m, exposes git to the LLM as a typed surface — not a string it can stuff flags into, but a closed vocabulary of actions (commit, rebase, restore-path, …), each classified: does it move a ref? is it safe in a shared worktree? is it recoverable? A junior agent implemented the restore-path verb — spec: restore these files in the working tree to HEAD, index untouched, recoverable via the journal — as git stash push.

Which moves a ref (refs/stash). And resets the index. And makes recovery depend on a stash stack instead of our journal. Three properties the classifiers stated, contradicted by the implementation four hundred lines below — and the build stayed green, because every theorem we had quantified over the typed action, and the handler’s argv was assembled inline in the IO body, where no theorem could see it.

The fix was pleasant enough: factor the argv into a pure function, pin it with a kernel-checked theorem. git restore --source=HEAD --worktree -- <paths>, exactly this shape, provable by rfl, regression now a build error. We’d done the same thing once before, for the same reason, when a startPoint argument was silently dropped on the floor by a handler whose validate arm parsed it and whose IO body ignored it.

Then I asked for the obvious generalization: do it for every git verb. One pure function, gitArgv : GitAction → Option (Array String), forty-odd constructors, and one theorem saying the first token of the assembled command is always the verb the type declares — no branch name, no path, no commit message can ever occupy the command position, and no handler can ever again run stash where the type says restore.

The agent wrote the forty-arm function in a few minutes. Then it spent six rounds failing to prove the theorem.

The struggle is the signal

Watch what the proof attempts actually looked like, because the texture matters. simp with the obvious lemmas: eight unsolved goals. Case-split on the action, then on each embedded option and boolean: subst fails — the equation isn’t of the form the tactic wants, because in arms like add the argv is #["add"] ++ paths.toArray and the head of an append with an abstract tail isn’t a computation, it’s a lemma. Split harder: now the match inside some (…) in the log arm needs its own split, behind a let. Every round of tactic archaeology dug up another arm doing something slightly different from its neighbors.

At that point there are two moves. The traditional one: grind. Find the right append-head lemma, name every case, write the forty-case proof, feel accomplished. It would have worked. It would also have been a proof that has to be maintained — forty cases of it, each ready to break the next time someone adds a verb.

My collaborator asked the better question: why isn’t this rfl? Tell me why, and then we refactor the code until it is.

The answer, once stated, embarrassed the code. The theorem “argv position 0 is the verb word” was, in that forty-arm function, a coincidence. Forty arms each independently spelled a literal ("commit", "rebase", "stash"…), and a separate table declared what the verb should be, and the theorem asked the kernel to verify — pointwise, through every if and match and let — that two parallel hand-written lists happened to agree. Of course the proof was miserable. The proof was doing the work the code structure refused to do.

The refactor is three lines:

def gitVerbWord : GitAction → String        -- the verb, stated once
def gitArgvTail : GitAction → Option (Array String)  -- flags + operands only
def gitArgv (a : GitAction) : Option (Array String) :=
  (gitArgvTail a).map (fun rest => #[gitVerbWord a] ++ rest)

The verb is now in the assembly. There is no second copy to disagree with. The theorem “the head is the verb” stopped being a forty-case coincidence and became a one-case consequence of the shape — the entire proof is: invert the map, take the head of a literal cons. It cannot rot, because the property is no longer checked against the code; it is how the code is built. And the forty-arm table that remains, gitArgvTail, now says only what actually varies per verb — which made it shorter and more readable than what it replaced.

The proof didn’t just get easier. The code got better. Those weren’t two effects; they were one effect observed twice.

Seven times is a method

Here’s why this post exists: that session was not novel. Going back through our own records, we have hit this exact sequence — theorem fights, code refactored, theorem trivial — at least seven times in one project’s lifetime, and we wrote several of them down before we recognized them as instances of one thing.

Different subsystems, different years, different agents doing the work. Same arc every time: the proof resists; the resistance, read correctly, is a location; at that location there is a design decision the code made carelessly; make it deliberately, and the proof stops resisting.

The degenerate cases fit the pattern too. Sometimes a proof looks impossible and the code is fine — then the difficulty is a structural artifact, and isolating the claim makes it compute (we once watched an apparently-hard lookup become rfl the moment it was stated as its own lemma). And sometimes the hard case is guarding something genuinely load-bearing — then the honest fix is a precondition that names it, and the proof difficulty has taught you which two lines of your encoder are security-relevant. Either way you learn where the complexity actually lives, which is more than the passing proof would have told you.

Why this works

Nothing here is mysterious once you say it plainly. A proof must formalize everything the code actually does. Clean, direct code gives the prover little to say; every conditional, every coupling, every clever reuse of state gives it a case. So proof effort and hidden complexity aren’t correlated by accident — they are the same quantity measured through different instruments. The runtime pays for complexity in bugs, the reader pays in comprehension, and the prover pays in cases; reduce the complexity and all three bills drop at once.

Which is why the anecdote we keep retelling internally cuts so deep. An automated-reasoning practitioner we know of spent years, with a team, proving properties of a production hypervisor. Later he wrote a substantial OS component from scratch and proved properties about it in about a month — a two-orders-of-magnitude difference he attributed to better tools and accumulated skill. We think the dominant term was neither: his fresh code was simply better than the hypervisor’s accreted code, and the proofs got cheap because the code got clean. Proof-difficulty had been measuring code quality the whole time; he read the gauge as “proving is slow” when it said “this code is complex.” When we’ve floated this reading to working verification people, they mostly don’t buy it — proof effort is treated as a property of the proof task, not a diagnostic of the artifact. We think that’s a blind spot, and it’s the blind spot this post is about.

Who found this before us

Old masters first. Dijkstra spent the 1970s insisting that a program and its correctness proof should be developed hand in hand — A Discipline of Programming derives programs from their proofs, and in EWD1243 he marvels, looking back, at “how closely program design and proof design would come together.” Hoare’s most quoted sentence — make it so simple that there are obviously no deficiencies — is this post in one line, if you read “obviously” as “with a short proof.” The intellectual priority is theirs, completely.

But notice the direction. Dijkstra’s discipline is prescriptive and forward: derive the code from the proof, and you’ll never write the bad code at all. Almost nobody programs that way, and almost nobody ever did. What we’re describing is the diagnostic converse, available to people who write code the ordinary way first: let the proof attempt fail, and read the failure as a code review. Dijkstra tells you where to start; the smoke detector tells you where you went wrong after you didn’t start there.

The seL4 project — the verified microkernel, still the largest sworn-in success of code-level verification — lived both directions and documented it. The SOSP paper says it plainly: “we discuss the kernel design we used to make its verification tractable.” Their papers describe redesigning kernel subsystems specifically to be provable (interrupt points, for instance, are an explicit knob trading proof complexity against latency), and report the dividend we’d predict: once the design was proof-shaped, re-verification after a change cost effort “roughly proportional to the size of the change.” Design-for-verification is real and they proved it pays. What the seL4 literature treats as project methodology, though, we’re claiming as a per-function, per-afternoon practice: not “architect the system so the proof is possible” but “this one theorem is ugly today, so this one function is wrong today.”

The type-system community has the nearest folk theorem. Yaron Minsky’s make illegal states unrepresentable and Alexis King’s parse, don’t validate are exactly our refactor in miniature: move a property from checked (a proof obligation, a runtime validation) to structural (the type can’t express the violation), and the obligation evaporates. Our gitArgv fix is parse-don’t-validate applied to a theorem: the verb stopped being validated against a table and started being part of the value’s construction. What the typed-FP tradition lacks — through no fault of its own — is the gauge. In Haskell you refactor toward unrepresentability when your intuition says to. With a theorem prover in the loop, you get a number: the proof got longer this month. The needle moved. Go look.

There is also an academic literature on “verification refactoring” — transforming programs to make their proofs go through (Echo’s semantics-preserving transformations; SPARK-era work on refactoring to reduce proof obligations; recent LLM work that transiently refactors code, verifies, then restores the original). Respectfully, we think the transient version has it backwards: if the refactored program was the one you could prove, that’s the better program — keep it. The refactor isn’t scaffolding for the proof. The proof was a code review, and the refactor is you accepting the review.

The LLM-era neighbors are converging fast but on a different corner. Hillel Wayne’s Why Don’t People Use Formal Methods? is the classic statement of the cost problem we claim LLMs dissolve. Amplify’s The Agentic Mullet (2025) argues that with a kernel checking the result, it’s fine to let models “vibe-code” the proofs — infinite prover monkeys, if it compiles it’s correct. True, and we rely on it daily — but it treats the proof as a product to be manufactured as cheaply as possible. Our claim is about the failures: the six rounds the monkeys spend not finishing are not waste to be optimized away, they’re the most information-dense code review you’ll get that day. And the proof engineering literature (the empirical productivity studies that came out of L4.verified) measures proof effort carefully — as a cost to predict, not as a signal about the artifact under proof.

The seL4 team’s retrospective even quantified the relationship we lean on: proof size tracks effort linearly, and “the best way to improve verification productivity is to invest more effort into writing code such that the verification burden is reduced later.” Closest of all, a recent interview study out of UCSD (On the Impact of Formal Verification on Software Development) reports practitioners of automated verifiers restructuring their code to make verification tractable and codifying those changes in style guides — expert folk knowledge, which that paper set out to systematize. The diagnostic loop itself — read the failed proof as a review of the code, per function, per afternoon — still appears in none of them.

So: is the idea new? The pieces are old, some of them fifty years old. What we haven’t found anywhere is the assembled claim — treat proof difficulty as a live, routine code-quality metric; when a theorem resists, suspect the code first; refactor until the proof is trivial, and keep the refactor — stated as an operating rule and backed by a documented series of in-the-wild instances. If someone has written that post, we’d genuinely like to read it; the closest things we found are a paragraph of seL4 folklore and Dijkstra’s ghost, nodding.

Why now — the LLM changes the economics

Here’s the part that makes this a 2026 post and not a 1976 one.

The reason nobody used proof difficulty as a code smell is that proofs were too expensive to attempt casually. A smoke detector you can only afford to install after the building is on fire is not a smoke detector. When a proof costs a specialist a week, you only write proofs for things you already believe are critical, and when one fights back you grind it out, because the alternative — refactor the code and re-prove everything downstream — costs even more. At those prices, proof-difficulty-as-diagnostic is a luxury belief.

An LLM agent collapses the price. Our agent attempts the proof the moment the function exists; six failed tactic rounds cost minutes of wall clock and nobody’s morale. And that changes what the failure is. When a cheap, competent prover that has seen a million proofs fails six times in a row on your forty-arm function, the failure carries information — not “the intern is weak” but “the shortest honest description of this code is long.” The human’s job relocates to the one step the machine can’t do: reading friction as diagnosis, and deciding the code is wrong, not the proof. That decision — stop grinding, refactor — is, in our experience, still a human’s call, and making it well is a skill worth naming.

There’s a compounding effect, too. The refactor the proof demands is almost always toward fewer cases, one source of truth, properties by construction — which is exactly the code an LLM is best at maintaining and worst at corrupting. Proof-shaped code is agent-shaped code. Every time the smoke detector fires and we simplify, the next agent’s next change gets safer, and the next proof gets cheaper. It’s the only quality ratchet we’ve found that tightens itself.

There’s an economic corollary, which I chase down separately in The $11 Trillion AI Capex Mirage. If a cheap retry loop against a perfect checker is what actually buys you reliability, then reliability is purchased with commodity inference and good scaffolding rather than with frontier pretraining. Six cheap failures and a kernel beat one expensive success. That is a pleasant fact for people building verified agents and an unpleasant one for anyone counting on the frontier to stay scarce.

The rule

As we actually practice it:

  1. Before patching a misbehaving subsystem, try to state its core invariant. Not prove — state. If you can’t find the value the invariant is about — if the only honest sentence is “these four stores agree” — stop patching. The design has no subject for its own correctness sentence, and every patch will add a store. Ten minutes, available on day one.
  2. When a theorem is hard, suspect the code before the proof.
  3. Find what the code is doing at the hard case — something conditional, lossy, duplicated, or coupled is sitting exactly there.
  4. If it’s gratuitous, refactor; the proof collapses, often to rfl. Keep the refactor — it was the point.
  5. If it’s load-bearing, write the precondition that names it. The proof just told you which lines are security-relevant; write that down too.
  6. Prefer structural proofs (rfl, simp, omega) over brute ones (native_decide on fixtures) because they stay honest: a structural proof only stays short while the code stays clean, so its length is a reading on the gauge. A brute proof pins the gauge at zero and tells you nothing forever.

The slogan version is the title. A theorem that resists is not a proof problem. It’s a bug report against the design, filed by the only reviewer on the team who is never tired, never polite, and never impressed by how clever the code is.

l3m is a coding agent written in Lean 4 whose tool contracts are kernel-checked; the git front-end episode above is commits a344d3d594 through 97412ad944 on its mainline. The internal note this post grew from — including the instances table — is records/notes/proof-difficulty-as-complexity-signal.md in the l3m repository.