Token-Based Formal Methods

Engineers make correctness arguments every day: this retry is safe because the handler is idempotent; this queue cannot grow without bound because the producer blocks on the same lock; the window never contains a repeated character because we move the left edge past each repeat. They show up in design docs, code review, and comments above tricky loops. They are the reasoning that actually keeps software working, and they are almost never written in boolean logic.

That is awkward, because formal methods have spent fifty years getting very good at checking correctness claims. They have proved kernels, compilers, and distributed protocols, and the proofs hold. But they check arguments written in a formal language, and the arguments above are not.

This series asks whether the gap can be closed from the other direction. Instead of translating people into a solver’s language, can we make ordinary engineering arguments checkable as they are?

The thesis

A natural-language argument can be checked like a program proof. Break it into small steps: two or three premises, one conclusion, one familiar inference. Name what each step uses and what it produces. The result is a proof graph. Its nodes can be checked one at a time, its wiring can be checked by ordinary code, and when something fails, the failure points at a particular claim rather than at the document as a whole.

The move underneath is narrower than it sounds, and I think it is the right way to read the current wave of work. Hoare logic never proved the implications inside a program proof; its rule of consequence hands them to whatever language the assertions are written in. For fifty years that delegate has been a decision procedure—a solver, a tactic library, a decade of automation. Replace it with a reader, and you inherit both the promise and the risk of this whole approach.

Why now

Because code production changed.

An agent returns a working diff in minutes. What it does not return is an account of the alternatives it weighed, the invariant it was holding, or why the boundary case is safe. Sometimes that reasoning was never written down; often it never existed in a form anyone could inspect. You inherit the code without its argument.

Tests do not fill the gap, because they never did. A suite reports on the cases someone thought to write. That was always partial evidence, and it was enough anyway—not because the sample was good, but because it was never the whole case. There was also an author who could explain the design and a reviewer who could weigh the explanation. The green check corroborated an argument that lived somewhere else. As code gets cheaper and its author less available, the passing test is asked to carry more trust than it can.

What is in the series

The old bargain looks at what formal methods deliver and what they charge: twenty person-years of proof against two of kernel, a specification nothing checks, and a certificate few people can read.
Token-based logic keeps Hoare’s structure and changes the assertion language. It argues for small steps, and shows the one composition move that turns up as Aristotle’s middle term, as Gentzen’s cut, and as sequencing in Hoare logic.
Does it work? tries the idea on one algorithm and one planted bug, looks at the two systems attempting this at scale, and reviews what is known about the reliability of the judge.

Where it ends up

This does not replace Rocq, Lean, or SMT solvers, and the people building it do not claim that it does.

The experiment in the last chapter is deliberately small: fifteen lines of code, proved twice—once as sixteen natural-language steps, once as 445 lines of machine-checked Rocq. The graph turned out to be a usable outline for the formal proof. It predicted where the hard part would be. And when the code was sabotaged, the failure landed on the node whose own justification had already identified the crucial guard.

The result it can defend is the negative one: this step breaks, and this input proves it. A counterexample is a fact, because the program ran. A positive verdict is a stack of fallible judgments, and a stack of judgments is only as good as its worst member. That limit is real, and I would rather state it plainly than argue around it. What is left is still worth having—a readable argument that fails in a named place, about a claim stated in the language its author actually thinks in.