If you can state it, you can probably prove it (July 2026)

A “year” of manifest-driven Lean, a cull of a hundred theorems, and the belief it overturned: proof is cheap; precise statement is the scarce resource. The corollary is a design heuristic.

I came to formal verification from statistics, and I brought a ladder with me.

The ladder was the one every working programmer knows. At the bottom, unit tests: cheap, concrete, you write a lot of them. In the middle, property-based or hypothesis tests: you state a general claim and let a fuzzer hunt for counterexamples. At the top, rarely reached and reserved for the truly critical, sat proof — expensive, slow, the province of people with type-theory PhDs. The folklore that came with the ladder was blunt: proving things in Lean is hard, and proving things about code is close to impossible.

I built a manifest discipline that encoded this ladder faithfully. Its evidence levels ran from Sketch (a name and a prose note, no formal claim yet) up through UnprovenConjecture (a precise claim, no proof) and TestedConjecture (a claim with passing test witnesses) to ProvenTheorem at the summit. The whole point of the middle rungs was to be a waiting room. Stating a property, I assumed, would be cheap; proving it would be dear; so there would be a large, useful population of stated-but-unproven claims, accruing value while they waited for someone with the time and skill to close them.

A LLM-year and a cull later, I think the ladder is upside down. Wall clock time, about a month.

The cull

The forcing event was mundane. I asked, of a codebase with a couple hundred kernel-checked claims: how many of these actually carry load? Not “how many compile” — all of them compiled — but how many would break if the thing they describe broke. How many are tripwires, and how many are ornaments.

The answer was brutal. We deleted roughly a hundred declarations across a dozen files, and not one deletion broke a proof, changed a build outcome, or removed a guarantee. What died:

The guarantees that actually mattered — that the tool registry can’t silently drift, that no code path reaches the filesystem except through a capability token, that undo restores what it claims to restore — were carried by a small number of real theorems whose statements were precise and whose proofs the kernel had genuinely closed. And crucially: nobody ever read those theorems. They work by failing the build when the world drifts out from under them. A tripwire you have to read isn’t a tripwire.

So far this is just good hygiene: we removed decoration. The interesting part was why the decoration had accumulated, and what that said about the ladder.

The two piles

When I sorted the claims that had languished unproven — the ones the ladder predicted would be a rich backlog of hard-but-worthwhile theorems — they fell into two piles. Neither was “hard theorem awaiting a hero.”

Pile one: precisely stated, already proven. Over and over, a Sketch whose doc-comment solemnly announced that its property “needs a formalism we don’t yet have” turned out to have a fully proven theorem about the very same function sitting ten lines below it. One Sketch gestured at the boundedness of a parser’s output; a parseStatus_bounded theorem right underneath proved that boundedness, universally, in a few lines. The Sketch wasn’t waiting for language. It was a tombstone — left behind after the real theorem had already eaten its subject. Wherever a property had been stated precisely enough to typecheck as an honest ∀ over data the kernel could see, the proof had usually been a short walk away, and had already been taken.

Pile two: unprovable because unstatable — and unstatable because of state. The claims that genuinely resisted proof resisted statement first. And when I asked why they couldn’t be stated, the answer was always the same shape. The property was about state the type system couldn’t see: a concurrency interleaving, a global variable that officially shouldn’t exist, the behavior of an IO boundary — git, the operating system, the terminal, the language model itself. You cannot write a clean Prop about “what happens when these two writes race” without first building a model of the racing, and building that model is the entire cost. These claims don’t belong in a proof backlog at all. They’re either assumptions about a foreign system — which deserve to be named as such, with a falsifying observation attached — or they’re prose, and a comment carries them better than a fake theorem does.

Put the two piles together and the ladder inverts. The scarce resource is precise statement, not proof. The middle tier — precisely-stated-but-genuinely-hard-to-prove — was nearly empty, because in this domain statement and proof collapse into the same step. State it and it’s proven; can’t state it and there’s nothing to prove.

Why the folklore is half true

“Proving things about code is nearly impossible” is not a myth. It is a precise description of one style of programming and a poor description of another.

In a state-machine style — mutable objects, sequences of commands, hidden global state, effects everywhere — the interesting properties really are about sequences of mutations. To state them, you must first reify the state and the transitions into a model, and then reason about paths through that model. This is genuinely hard, and it is where the reputation of formal methods was earned. The pain is real.

In a functional style — immutable values, functions without side effects, effects pushed to a thin shell at the edges — the interesting properties are equations and structural invariants over data. “This transformation is idempotent.” “This output’s length is bounded by its input’s.” “Parse and print round-trip.” The type already carries most of the argument, and the kernel closes the rest cheaply. There is no model to build, because the data is the model.

Almost every genuinely painful moment in the year of building — and almost every property that would not go quietly into a theorem — traced to state that had leaked in against the grain of the design. Concurrency I had tried to avoid and hadn’t fully. A global that was nominally illegal and had crept back. An IO seam that had grown wider than it needed to be. State is the thing that is hard to reason about. Proof, over functional data, is easy.

The heuristic

This is the part that changed how I work, and it has nothing to do with verification per se.

The difficulty of stating a theorem is a signal about the code, not about the theorem.

When a property is awkward to state, the reflex the old ladder trained — “reach for a heavier proof technique, or park it on a lower rung until we can afford the proof” — is exactly wrong. The productive move is to treat the awkwardness as a design smell and restructure the code until the property becomes easy to state. Concretely, that almost always means the same thing: push the state out of the core and into a thin IO shell, and express the core as functions over immutable values. Do that, and the property that was unstatable becomes an equation. And the equation is usually a few lines from proven.

So the workflow I stumbled into is not a verification tactic. It’s a design discipline:

Think about the theorem first. If the theorem is easier to state, you have found the better design. The proof is a byproduct.

The manifest layer, which I built to be a proof repository, turned out to earn its keep as a design forcing-function. Every time I reach to add a claim and find it awkward to phrase, that friction is the layer doing its most valuable work — sending me back to the code before I’ve written a line of proof. A “no, I can’t state this cleanly” is not a verification limitation to be documented and deferred. It’s a code review comment I’m writing to myself.

A worked example, live

The heuristic keeps earning its keep, and the most recent case sharpened it in a way the “push state out” framing didn’t quite capture. The code was already functional — pure values, no leaked state — and the proof was still hard. The friction was pointing at something finer.

The task was a context-compaction planner: when a conversation grows too long to fit the model’s window, decide which old turns to summarize. The first design took the transcript as a flat list of messages and computed, by a backward-walking recursion, the largest “safe” cut point — safe meaning don’t split a tool call from its result. Pure function, immutable input, no IO. By the old folklore, provable. By the new heuristic, it should have been easy.

It wasn’t. The two properties I wanted — the summarized chunk is contiguous and non-empty — fought every tactic. The proofs kept snagging on the backward-search recursion and a nested conditional that guarded it. I burned through a discouraging number of failed attempts before I stopped and asked the heuristic’s question: not “what heavier tactic do I need,” but what is this difficulty telling me about the design?

Two things, it turned out.

First: I was cutting at the wrong granularity. The whole reason the boundary needed searching was that a flat message list lets you cut anywhere, including halfway through a tool round — so the code had to hunt for a legal spot. Restructure the transcript as a list of turns, where a turn is an indivisible unit that already contains its tool round, and the search evaporates: every turn boundary is legal by construction. There is no unsafe cut to avoid, because the type no longer lets you express one. The backward-walking recursion — the thing the proof was choking on — simply deleted itself.

Second, and smaller: a redundant guard. After the turn refactor a proof still wouldn’t split cleanly, and the culprit was an if n ≥ keep then n - keep else 0 — a conditional protecting a subtraction that, in this language, already saturates at zero on its own. The if was dead defense, and the proof was failing to case-split on a branch that could never differ from the other. Delete the guard; the property becomes plain arithmetic; the tactic that closes it is omega.

Neither fix was “push state out” — there was no state to push. The friction was diagnosing shape: the wrong atom to cut on, and a guard that shouldn’t exist. Both properties are now short, real, kernel-closed theorems, and — this is the tell — the code that carries them is simpler than what I started with. Fewer functions, no search, no redundant branch. The proof didn’t just get easier; the program got better, and by exactly the amount the proof got easier.

That is the heuristic’s deeper form. “Push the state to the edges” is the most common way a design is bad. But the general law is broader: proof friction is a gradient, and it points downhill toward the better design — whether the fix is exiling state, choosing the right atom, or deleting a line that was never doing anything. Follow the gradient and you arrive at code you’d have wanted anyway; the theorem was just the instrument that found it.

The counterexample ran for two weeks

The planner story shows the gradient at fine grain — a proof that fought until the code got simpler. A second case, from the same codebase, shows the coarse grain, and it sharpens the heuristic into the form I now think matters most. In this one, no proof was ever attempted. That was the signal, and it went unread for two weeks.

l3m has a subsystem for firing swarms of read-only reader agents at a batch of tasks — fire up to seventy-two, harvest their reports, fill the holes, repeat until done. It broke, and its author — the agent who built it and owned it — spent two weeks patching it. The bug list reads like a distributed-systems war story: reports dropped in git compare-and-swap races; task rows stuck in status: "running" forever; a drain stalled at 342 of 400 with the pool insisting no slots were free; phantom in-flight workers; a stuck completion guard. Five bugs. Five patches — a self-heal pass, a fallback heuristic, a no-progress counter, a min of two counts that should have been equal. After each patch, a new bug.

The diagnosis, when it finally came (in an honest proposal written by the owner, which is its own lesson), was that the five bugs were one bug. The state of the computation lived in four places at once: a result field in a task file, a status field in the same file, a live-thread count in an in-process registry, and a git branch where every reader published its report. Each bug was those stores disagreeing. Each patch added reconciliation machinery — which is to say, added a new way to disagree. The readers were in-process threads with perfectly good return values; the design had them publish to a git branch instead, which a control loop folded back into a file, which it re-read to guess the system state. A thread pool had been built as a distributed system by accident, and it came with the full complement of distributed-systems hazards, none of them paid for on purpose.

Here is the test that would have caught it on day one. Try to state the core invariant. The property you want is first-write-wins: a completed reader’s verdict is recorded exactly once, and a late duplicate cannot overwrite it. Write that as a theorem about the old design and you hit the wall before the proof — before the statement. First write wins in which store? The file’s result field? The registry? The branch? There is no value in the program that is the pool state; it exists only smeared across two files, a ref, and a git ref, materialized transiently inside the very heuristics that keep guessing it wrong. The theorem has no subject. The only honest statement is “the four stores agree” — a consistency property over IO traces, which is pile two exactly: unprovable because unstatable, unstatable because of state.

The rewrite collapsed the four stores into one value: an array of optional results. none is a hole, still fireable; some is a verdict. That’s the entire state. First-write-wins became a one-line simp, because the fill function is a match on the slot. Nine invariants in all — hole-counting, capacity, budget, the drive decisions — and none needed more than simp and omega. The proofs arrived at that difficulty before the new drain was wired to anything, which is the point: they were the design review. The old machinery — the self-heal, the counters, the reconciliation — was then deleted wholesale, and each of the five bugs is now not merely fixed but inexpressible.

What this case adds to the heuristic: the signal comes in two strengths, and they arrive at different times.

Weak signal: you can state the theorem, but the proof fights you — induction over a recursion that shouldn’t exist, case splits on a guard that defends nothing. Reshape the code. That’s the planner story.

Strong signal: you reach for the statement and find there is no value to state it about. The property is only expressible as “these N places agree.” That is not a proof difficulty; it’s the type system telling you the program’s state lives in the world instead of in a value. And unlike the weak signal, this one is available on day one, before any proof is attempted, for about ten minutes of effort:

When a subsystem starts eating patches, stop and try to state its core invariant. If you can’t find the subject of the sentence, stop patching — every fix will add another store to the consistency property you already can’t write.

Two weeks of failed fixes were the price of not asking the question. The question costs ten minutes. The blocker was never provability — the nine proofs, in the end, were trivial. The blocker was stateability, and the missing definition — the value that is the pool — was both the diagnosis and the cure.

What survived

The discipline came out of this smaller and, I think, more honest. Where it once had a spectrum of evidence levels papering over the gap between “I can gesture at this” and “I have stated this precisely,” it now recognizes essentially three load-bearing forms:

The lower rungs still exist in the library for genuine rarities, but the default palette is those three, and I’m suspicious every time I reach past them. A manifest full of Sketches isn’t a backlog of proofs waiting to be written. It’s a backlog of design smells waiting to be resolved.

I came for the proofs. I stayed for what wanting the proofs did to the code.

If the asymmetry holds outside this project — proof cheap, precise statement dear — it has a price tag attached, which is the subject of The $11 Trillion AI Capex Mirage. Compute buys the cheap half. The scarce half is a human sitting still long enough to say exactly what they meant, and there is no cluster you can build that does that for you.

This overturns some advice in two earlier posts — the Sketch placeholder in Manifests as Specs, and the framing of vacuous claims as minor in Reading a Library from Its Manifests. I’ve left those posts standing with correction notes rather than rewrite the record; being wrong in public and saying how is part of the point. The underlying machinery is lean-manifests; the agent it grew up around is l3m.