If you can state it, you can probably prove it

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 year and a cull later, I think the ladder is upside down.

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.

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.

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.