A linter that redoes the work catches injected errors that self-verification misses

A reasoning trace contains the equation total = 16-3-4 = 8, then a check: the value of that equation is 8. Check and equation agree. A language model asked to verify the trace reads along, tells itself that 16 minus 3 minus 4 equals 8, and signs off. The subtraction is still wrong.

When a long chain of thought ends in a wrong answer, there is no unit test to run on it, just prose to hunt through. The usual remedy is a second language model that comments on each step and votes on whether the trace hangs together. It handles the easy errors and stumbles on three kinds that come up often in math: a variable used before it is defined, a unit dropped mid-derivation, two equations that give one name different values. Rerun at temperature zero, it also changes its verdict on roughly a tenth of traces.

In the paper we stopped asking a second model to read more carefully and changed what the first one writes, so that a program can redo the work.

A trace a program can parse

Janet has 16 eggs, eats 3, bakes with 4 and sells the rest at $2 each:

GIVEN:
  total := 16
  eaten := 3
  baked := 4
  price := 2 [USD]
GOAL: revenue [USD]
STEP[s1]: subtract used eggs
EQ[e1]: sold = total - eaten - baked
CHECK[c1]: arith: e1.value == 9
EQ[e2]: revenue = sold * price
CHECK[c2]: arith: e2.value == 18
ANS: 18 [USD]

A linter builds a scope from the GIVEN block, substitutes into e1, gets 9, and compares that with the 9 asserted in c1. Had the model written e1.value == 8, the linter would compute 9 and report error TE_E007 on that line. No model is consulted.

We call the format Telegraph Reasoning. Its seven tags cover inputs, the goal, a one-line natural-language step, an equation SymPy can parse, a verification claim, case splits and the answer. The grammar is deliberately spare.

Seven of the linter’s eleven rules are structural: they need only the parse tree and check things like tag order, backward references, and no “maybe” or “wait” inside a tagged line. The other four hand the trace to SymPy:

• Scope. Every symbol is declared in GIVEN or defined by an earlier equation.
• Units. An equation’s declared unit matches the unit its right-hand side produces.
• Numbers. Where an equation’s right-hand side resolves to a number, it equals the declared left-hand side.
• Checks. Every CHECK claim holds when recomputed from the trace.

The last rule is the break from self-verification as Natural Program practises it. Natural Program asks the model whether its step holds. The linter recomputes what the model claimed.

Recomputing beat rereading

We built 266 traces to measure checking rather than solving. Of these, 196 carry exactly one injected error from five categories (arithmetic slip, lost variable, unsupported conclusion, wrong unit, contradicting equation), mostly introduced by a script into correct traces that Claude Sonnet 4.6 had written; the other 70 are clean. Four checkers read every trace. Natural Program saw them rendered as prose by a fixed mapping, and the judge (Sonnet 4.6 again) saw them in their tagged form; both model-based checkers ran three times at temperature zero with a majority vote.

Checker	Injected errors caught	Clean traces flagged
Structural rules only	0.0%	0.0%
Full linter with SymPy	99.5%	10.0%
Natural Program self-verification	66.3%	2.9%
Sonnet 4.6 as judge	87.2%	5.7%

The linter caught 195 of 196: 33 points ahead of self-verification, 12 ahead of the judge, both significant after correcting for multiple comparisons. On their own, the structural rules caught nothing, so all of the catching came from the four rules that compute.

The gap opens where checking is computation

Self-verification came within nine points of the linter on unsupported conclusions. On the bookkeeping categories it fell away, catching about half the lost variables, half the contradicting equations, and 2 of 12 wrong units against the linter’s 11.

A unit error shows why. A trace writes EQ[e2]: distance = speed * time [miles], with speed in metres per second and time in seconds. The self-verifier knows the formula and signs off. The linter is more literal. It multiplies the units, gets metres, sees miles, and fires TE_E005. Name resolution, symbolic substitution, a unit registry: a language model approximates these by judgment, and the linter just runs them. The judge landed in between, matching the linter on contradicting equations yet missing about one arithmetic slip in seven.

One rule carried the largest load

Switching off the numbers rule dropped detection from 99.5% to 78.1%; 42 of the 196 errors were caught by it and by nothing else. Switching off the checks rule, which we think of as the conceptual heart of the design, cost 2.6 points. Unlike the checks rule, the numbers rule does not depend on the model writing a check line. It runs on every equation whose right-hand side resolves to a number, and it fires even when the model’s own check agrees with the slipped value. It is the rule that settles the opening trace: substitute into 16-3-4, get 9, compare with the asserted 8, raise TE_E006.

Same trace, same verdict

The linter is deterministic by construction: one trace, one set of flags and line numbers, on every run. Across three runs at temperature zero, self-verification flipped its verdict on roughly 10% of traces and the judge on roughly 7%. For a pipeline that routes flagged traces to remediation, that is the difference between a unit test and a vote.

It is also fast. The median trace lints in 9 ms and the whole corpus in under 3 seconds on one CPU, where each model-based checker needed about 25 minutes.

The linter does raise more false alarms: 7 of 70 clean traces, the highest rate in the table. Two of those flag internal inconsistencies in traces whose final answer still matched the gold label; counting them as catches gives 7.1%. The other five each have a documented fix planned for the next version, and among them are parametric problems that leave a parameter undeclared on purpose.

Checking can leave the model

For anyone who audits model reasoning, this splits verification in two. The part that is computation can move out of the language model, once the model writes in a format a program can parse. The price is the format, and following it was not the hard part: prompted with five examples, Sonnet 4.6 wrote structurally valid traces for every GSM8K problem and 96.4% of MATH500. Telegraph Reasoning is a substrate, not a rival to reinforcement-learning methods that shorten traces; those cut tokens without making a trace any more checkable.

Structure in place of free prose is also the idea behind Telegraph English, which rewrites text into atomic fact lines so that compressed text doubles as an index. A linter this fast fits inside training, too. Why Additive Process Rewards Wash Out measures what group-normalized reinforcement learning does to process rewards. Doing so needed a verifier quick and deterministic enough to instrument every reward call, and a rule-based trace linter with the detection rates above did the job.

What we have not shown

The corpus is synthetic, its errors injected in categories chosen to match the linter’s rules. So 99.5% measures how well the rules catch what they were built for, and we do not claim it transfers to the mistakes models make on their own. What we expect to carry over is the mechanism: re-evaluating an equation catches a slip that the model’s own check repeats.

Everything is math, and one model did all the generating and judging; logic, code and cross-model checking are untested. Version 1 of the grammar cannot express composite units that add inside a product, brute-force case enumeration or quantifier-heavy logic, and the one missed wrong-unit error traces to these gaps.

The format costs accuracy on harder problems. It matched natural-language chain-of-thought on GSM8K within a point but trailed concise chain-of-thought by 5.80 points on MATH500, a deficit our pre-registration marked as real; about half of the format-specific failures there are notation mismatches between LaTeX and SymPy. The comparison is uneven, too: five examples in our prompt, none in the baselines’, and no matched-shot run yet. Tagged traces also spend about three times as many tokens per correct GSM8K answer as concise chain-of-thought. And a preliminary attempt to fine-tune the format into a 2B model lost accuracy against the same model prompted for ordinary chain-of-thought.

The deepest open question is what passing means. Every rule checks the trace against itself; none reads the problem statement or the answer key. In Measuring Answer Accuracy and Trace Verifiability we trained a small model with outcome-only reinforcement learning to write a compact trace language that a program evaluates, and a trace the checker accepted was correct only about one time in three. Telegraph Reasoning makes consistency cheap to establish. Correctness still has to be measured on its own.