The green theorem that guards nothing (September 2026)

Three times in one week we found a kernel-checked proof standing guard over code that nothing executes. The failure has a shape, the shape has a fix, and the fix only became sayable when our main loop became a nameable function. This is the confession, and the way to reason about it correctly.

In an earlier post I argued that in a functional codebase, statement is the scarce resource and proof is cheap: state a property precisely over data the kernel can see, and the proof is usually a short walk away. I stand by that. This post is about the trap on the far side of it — what happens after the proof, when the theorem is green, kernel-checked, counted in the trust report… and guarding nothing.

We hit it three times in one week, in three unrelated subsystems.

The three incidents

Incident one: the undo algebra nobody calls. Our agent’s /undo is backed by a small calculus of file mutations — edit, create, delete, each carrying the prior content. Its reverse is total and involutive, kernel-proved. Inverses are anchored: each records what the file must contain now for the undo to apply, so “an undo cannot fire on drifted state” is structural, not a runtime hope. Eighteen theorems, all real, all green. A coverage script asked the obvious question — how many executed effects flow through this calculus? — and printed its own diagnosis: “the calculus is correct, closed, involutive, kernel-proved, and NOTHING FEEDS IT.” reversibleSites=0. The /undo users actually invoke is a git checkpoint restore — eight subprocess calls ending in reset --mixed — which has zero theorems. The proven path and the executed path had never met.

Incident two: identity resolution, proven but unwired. A boot-time identity bug once bit us: an embodied resume dropped a persona mask. The fix came with a work order — a pure resolveIdentity whose body has no embodiment branch, plus a theorem, resolve_ignores_embodiment, red if anyone reintroduces the carve-out. Both were faithfully ported to V2. An audit then found that V2’s boot path never calls resolveIdentity and never constructs the environment it takes. The theorem is green. The bug it exists to prevent could return tomorrow, uncaught, on the live path — which resolves identity its own way, three modules over.

Incident three: the executor under the proven planner. /undo’s planner is genuinely verified: which turn to land on, which commit sha, whether the branch move is divergent — pure functions with kernel-checked theorems. Then the plan is handed to an executor that shells out to git, and the executor has no theorems at all. Trust chain: proven plan → unproven doer → axiomatized git. Nobody had noticed the middle link because the report counts theorems, and the planner has plenty.

Three subsystems, one disease. And note what the disease is not: not a false theorem, not a proof error, not statement imprecision. Every proof is real. The theorems are just about code the program doesn’t run.

Whose fault? (Partly the manifests’.)

My first suspicion was the manifest discipline itself — by giving theorems a home of their own, had we made it easy for them to drift away from the code? On reflection: proximity is innocent, but the bookkeeping is not.

Proximity is innocent because in all three incidents there was no call site for the theorem to sit next to. The defect was precisely that nothing calls the proven function. A theorem in the same file as its subject is still only an observation about that code; the IO shell three modules away is free to reimplement the logic inline, and no amount of adjacency makes the reimplementation visible.

The bookkeeping is guilty because it made proof volume legible and proof reach invisible. The trust report counts kernel-checked claims — a number that goes up, feels like progress, and is checked by CI. It has no column for “consumed by the executable.” So we built an incentive gradient where proving is measurable work and wiring is not, and three teams slid down it independently. The report was honest about every individual claim and misleading about the system.

The two quantifiers

Here is the way to reason about it correctly, and it turns on noticing that two different ∀s live at two different levels.

Level 1: the theorem’s own ∀, over inputs. ∀ m s, reverse (apply m s) = s — quantified over values. This is the quantifier Lean’s logic handles natively, and it was never the problem. All three dead theorems have impeccable level-1 quantifiers.

Level 2: the architectural ∀, over occurrences. What you actually want is: for every place in the executable where a file gets restored, the restoration is the one this theorem constrains. That quantifier ranges over call sites — over the program itself — and an ordinary theorem cannot state it, because the ambient program is not a term the program can quantify over. This is why the property feels unsayable when you first reach for it.

The tempting patch is reachability: check that something on the executable’s call graph consumes the proven function. But reachability is an ∃ — one witness, somewhere — and an ∃ cannot carry a guarantee. One blessed path through the proof proves nothing about the other paths; the backdoor is precisely the path you didn’t sample.

The architectural ∀ is sayable. Not as a proposition about behavior — as a closure property about introduction and elimination rules. Two mechanisms, and we had both in the tree before we understood why they mattered.

Mechanism one: the mint

Make the proven function the only constructor of a type the downstream path requires.

Concretely: give the undo executor a signature that demands a RestorePlan, and make RestorePlan’s constructor private — mintable solely by the verified planner. Now “every restore is a planned restore” needs no audit, no reachability check, no discipline. The type has no other introduction rule, so every term of that type — anywhere, forever, including code written next year by someone who has never heard of the theorem — factored through the proof. To possess the value is to have paid the toll.

The ∀ over call sites is discharged by exhaustiveness of introduction. The elaborator, not a reviewer, is what says “all.”

We had two live examples before we named the pattern. A typeclass instance whose restores field is the round-trip proof — the instance cannot elaborate without it, so “file mutations are reversible” became, as the file puts it, an un-forgeable elaboration fact rather than a stored claim. And a pair of runtime types made mintable only by their own functions — a clipped tool result, a resolved fuel budget — so no code path can hold a Clipped it didn’t get from the clipper. That’s the mint. The fix for incident two is the same move: make boot identity a value only resolveIdentity mints, and the unwired theorem becomes a compile error instead of an audit finding.

Mechanism two: the closure

Some effects can’t be gated by a value — anyone can spawn git reset as a subprocess; possession of no token is required. For these, the architectural ∀ takes its other honest form: enumerate the elimination sites and prove the set is closed.

We already knew how, from a different fight. Our capability boundary is enforced by theorems of the shape “no code reachable from main calls IO.FS.* except through the filesystem capability” — kernel-checked over generated call-graph data, rebuilt every time the graph changes. That is an architectural ∀ written in the contrapositive: rather than “all filesystem writes are capability writes,” it says “a filesystem write outside the capability does not exist,” and the build fails on the counterexample. The undo analogue is one closure fact — the only caller of the raw reset primitive is the executor, and the executor’s signature demands a RestorePlan — splitting the guarantee into the piece the call graph proves and the piece the type proves.

Why we couldn’t say this before

There is a precondition hiding under both mechanisms, and it took us embarrassingly long to see it: your program has to be a term before you can quantify over it.

“No code reachable from main does its own IO” is only a statement if main names a function and the call graph under it is data the kernel can inspect. In a codebase organized around mutable globals, initializer magic, and an event loop assembled at runtime, there is no term to close over — the architectural ∀ isn’t false, it’s unstatable, which is worse. We spent a long campaign driving our agent’s global mutable cells to zero and making the REPL a pure function of its inputs, for reasons that at the time were mostly about resume semantics. The unadvertised dividend is this post: once the loop is a nameable term, “reachable from main” is a proposition, the contrapositive closure theorems become writable, and the mint pattern acquires teeth — because a private constructor only guarantees uniqueness of introduction if there’s no reflection backdoor or init-time mutation to forge a value behind the elaborator’s back.

Functional style doesn’t just make level-1 theorems cheap, which was the last post’s claim. It makes level-2 theorems exist.

The residual ∃, and the honest scorecard

One footnote, because it rescues the despised existential. A mint-∀ can be vacuously true: if nothing ever constructs a RestorePlan, then “all restores are planned” holds over the empty set while /undo does raw git on the side. So the honest form is a pair: the ∀ by mint or closure, plus one ∃ witness of non-vacuity — evidence that the live path actually mints one. Reachability was never the guarantee; it is the guarantee’s non-triviality certificate. (Our manifest rules already impose exactly this anti-vacuity discipline on tested claims; the surprise was needing it for architecture.)

So the scorecard we’re moving to, per load-bearing theorem:

Level-1 ∀ — the theorem itself, kernel-checked. (We had this.)
Level-2 ∀ — its subject is the unique introduction (mint) or the eliminations are closed (call-graph contrapositive). (This is what died, three times.)
Non-vacuity ∃ — the live path constructs at least one witness.

A theorem with only level 1 is an observation. All three levels make it an enforcement. The trust report needs a column that says which — because we have now measured, three times in one week, exactly how much a green check mark can mean without one.

The moral

The folklore says the hard part of verification is proving. The last post said no — the hard part is stating. This post is the third turn of the screw: after you can state and you can prove, the remaining failure mode is that the program is not obligated to use what you proved. Proof creates knowledge; only architecture creates obligation. The mint and the closure are how you write the obligation down, the nameable main loop is what makes them expressible, and the one-witness ∃ is how you know you haven’t achieved perfect safety over the empty set.

A theorem you don’t wire to the program is a tombstone with excellent epitaph hygiene. We keep finding our best writing on tombstones. The fix is not better theorems; it’s making the executable unable to compile without walking through them.