Cheng Tan

Does It Work?

One algorithm, a planted bug, and the limits of using a reader as an oracle

· systemsresearchai ·中文

Arguments about reasoning are cheap, so I built the smallest experiment that could embarrass this one: take a fifteen-line algorithm, prove it twice (once as a graph of natural-language inference steps, once mechanized in Rocq, formerly Coq), and compare.

The algorithm is the sliding-window scan for the longest substring without repeated characters. A left pointer, a running maximum, and a map from each character to its last position. No cleverness anywhere, and one guard carrying the entire correctness argument: if the current character was seen at or after the left edge, advance the edge one past that earlier occurrence.

Two proofs of the same fifteen lines

The first proof has sixteen nodes, S1 through S16, each a small inference with two or three premises, one conclusion, and a short justification. Edges are typed by how a conclusion gets reused: as a direct premise, as the inductive hypothesis, as one arm of a case split that rejoins by disjunction elimination, as the base or step of an induction, or as one conjunct of the final verdict. Structurally it is a Hoare proof—an invariant, a base case, an inductive step with a two-way split on the last-occurrence lookup, and a rule of consequence composing into the postcondition.

The claim-level proof graph: sixteen syllogism-grade nodes. A base case and an inductive step, whose two cases rejoin at S11 by disjunction elimination, close the induction at S12; five independent lemmas then conjoin at the verdict. Edges are typed by how a conclusion is reused, which is what lets ordinary code check the wiring.

The second proof establishes the same theorem in Rocq, with no axioms and nothing left admitted. It runs 445 lines against the algorithm’s fifteen, roughly twenty-nine to one, across 29 named lemmas, and took four compile-debug cycles to land.

Three results came out of the comparison, and only one was expected.

The graph made a good outline. The Rocq proof was written top-down from S1 through S16 in essentially one pass, and the invariant’s seven conjuncts are the graph’s inductive-step nodes almost verbatim. The structure crossed the language boundary at about zero cost, which is what you would predict if the middle-term discipline really is indifferent to which level you work at.

Formalization found no error in the graph. All four debug cycles were tactic and bookkeeping work, not changes to the reasoning. Thin evidence, but it suggests a disciplined graph can serve as a practical first draft of a formal proof.

The graph predicted the hard part. About 42% of the Rocq lines were index and list bookkeeping no reviewer would ever doubt. The conceptual difficulty sat where the graph said it would: maximality, the obligation that the left pointer is minimal and not merely legal. Which suggests a workflow. Keep the graph as the main artifact and formalize only the two or three high-risk nodes.

One example, chosen by the person making the argument. I will come back to that.

The planted bug

A proof you cannot break is not evidence, so I weakened the guard by one character. The broken version advances the left edge only when the earlier occurrence lies strictly after it, rather than at or after.

That fails when the earlier character sits exactly on the left edge: the window keeps a duplicate and the reported length can be too large. On "aa" the buggy program reports 2, though no duplicate-free substring of "aa" is longer than one character.

The graph flags the guard node. Its justification had already named that boundary as essential—before anyone touched the code, it said in as many words that a strict comparison would fail to advance the pointer in exactly this case. Then the counterexample stage stops arguing and runs the program. Verdict: REFUTED, with a failed claim and an executed witness.

That is a localization result, not a soundness result, and localization is what neither of the usual tools gives you. A test says something is wrong. A machine-checked proof says nothing is wrong. A proof graph says where, in a sentence a reviewer can read—which is precisely the property De Millo, Lipton, and Perlis said verifications lack. It is a message.

The asymmetry

Working through the implementation, the thing that struck me hardest was not a measurement. It was which stages need a model and which do not.

Producing the graph needs one, and so does judging whether a node’s premises entail its conclusion. But checking that every premise reference resolves, that each rule gets the arity it declares, that leaves bottom out only in the precondition or the program’s own semantics: all of that is ordinary deterministic code. The counterexample stage asks nobody’s opinion either. It runs the program on inputs drawn from the precondition and compares against an executable oracle.

Which gives the central asymmetry: REFUTED is sound; PROVED is not. A counterexample is a fact, because the program ran. A positive verdict is a stack of judgments, and a stack of judgments is exactly as good as its worst member. A useful system needs a third value, INCONCLUSIVE, and a rule that it never silently passes.

That belongs in the headline rather than the caveats. It is the asymmetry that makes tests useful and their absence meaningless, with one addition: here the negative result arrives with an address.

What the research says

Two systems are attempting versions of this at a scale one example cannot reach. Both come from IPADS at Shanghai Jiao Tong and share an author, so they are one group’s bet rather than two groups converging.

FM-Agent moves the checking step: 522 new bugs across four systems and 277,000 lines of code in about two days, with no solver in the loop. The clever part is not the reasoning but the specification. FM-Agent derives each function’s contract top-down from its callers, so a buggy implementation cannot launder itself into its own spec. The one ablation is the number worth remembering: specs derived from implementations find 57 bugs where specs derived from callers find 339.

Those numbers need care. The 522 are reports that survived a filter; there is no published false-positive rate, and for two of the four systems the filter’s notion of expected behavior came from a machine-written specification. The authors disclaim the right things: “we do not claim FM-Agent can replace existing formal verification tools.”

SpecFS is adjacent but different. A multi-part natural-language specification, using pre- and postconditions and rely-guarantee contracts as a writing discipline, generates about 4,300 lines of C across 45 modules; the result fails 64 of 754 xfstests. Nothing is machine-checked: validation is regression testing plus a second model reviewing the first. In one line, FM-Agent replaces the prover with a language model and SpecFS replaces the programmer with one, and only the first is a claim about verification.

The recipe is not new in mathematics either. Pseudo-formalization (decompose a proof into modules, check each independently, aggregate) was published this year and beats handing a judge the whole proof, flagging about 60% fewer false steps at matching recall. Its own reported limit is the telling part: both verifiers still leave roughly half the known errors uncaught. Breaking an argument up helps; it does not make the judge trustworthy.

The benchmark picture is genuinely mixed. Frontier critics reach about 86.5% step-level balanced accuracy on expert-annotated competition-math errors, and verification rates consistently exceed solve rates—checking is easier than producing, which is the economic premise of this whole approach and appears to hold. But swap naturally occurring errors for adversarial ones (circular reasoning, plausible-but-irrelevant steps, deliberate deception) and the best score falls to 68.8% against a random floor of 50. Verdicts are unstable too: judges flip between 25% and 71% of the time under simple pushback.

The worst result is the last. When a solution reaches the right answer by invalid reasoning, frontier models score as low as 48% at catching it, below chance on a binary question, while humans lose only about six points relative to solving the problem themselves. The mechanism was measured rather than guessed: an answer-confirmation bias, in which the model checks for the right answer instead of checking each step. Patch the representation of the final answer and the verdict flips.

That is exactly the shape of a node check: you hand the judge a conclusion and ask whether the premises deliver it, and the judge can see the answer. The response is architectural, not rhetorical: deterministic checks wherever they are possible, judged steps small enough to sit inside the regime where judgment is reliable, and never a bare pass.

Where this could go

The first use case is not where formal verification already thrives. It is the ordinary argument in a design doc or a code review: why a retry is safe, why a queue is bounded, why a cache stays coherent. Nobody is going to write a Rocq specification for any of those. The alternative to a proof graph there is not Lean; it is no checked argument at all.

Three more. Proof maintenance: the cost center of verified systems is not the first proof but the second, after the code changes; a graph re-checks node by node and reports which claims the change invalidated, which is what 200,000 lines of Isabelle cannot tell you kindly. Review by parts: a design document that ships its argument as a graph can be disagreed with at node 7 rather than approved or rejected whole. Reviewing research: I have argued elsewhere that our field’s validation phase is the bottleneck, and part of why it is slow is that a paper’s argument is not checkable in pieces.

The ledger

What this rests on, stated plainly: one hand-picked algorithm. A checker that is itself a language model, with a measured 48% floor in the setting closest to node checking. Prior work that already reports leaving half the errors uncaught. And a system whose only defensible verdict is the negative one.

That last item reads like a deflation, and I want to end by refusing it. This step breaks, and this input proves it is more than any tool offers today for an argument written in English. It is local, it is readable, it is something you can act on—and unlike 200,000 lines of certificate, you can say it out loud in a hallway.

References