Every number below is a live ProveML claim.

The paper argues that an AI's claims should carry markup a machine can check. This page holds the paper to that: its findings are written in ProveML, and the fragment below is generated by a script that resolves every marked claim against the same experiment artifacts the paper's tables regenerate from. If a run were redone and a number drifted, that generator would refuse to emit the fragment — there is no hand-written path by which a number can reach this page unproved. And this page does not take the generator's word for it: at every build it verifies the same markup again, against the same store, with the ProveML package it ships. If the package ever changed its judgment, the page would refuse to build.

subject a record in the artifact store
verified equals the artifact value
a judgment whose registered rule holds

What the verifier itself catches

Before measuring any model, the paper measures the instrument. the detection study planted 20 deliberate errors in otherwise valid markup — wrong values, wrong entities, missing context, subtle canonicalization slips — and the verifier caught 20 of them: nothing slipped through. That is a conformance test, not a benchmark; exact comparison either sees a difference or there is none.

The mechanism is within reach of frontier models

Three models that were frontier in August 2026 — Claude Opus 5, Claude Sonnet 5, and the open-weight DeepSeek V4 Pro — over two benchmarks, three runs each: the frontier study. Across all its 342 query-runs, 0 answers came back empty or without markup: no empty answers at all. Claude Opus 5 opens at 86.5% first-pass verification on education (spread 0.3) and one correction pass lifts it to 94.8%; DeepSeek V4 Pro reaches 100% on finance on the first pass and covers 96.4% of its numbers, the strongest of the three.

What remains is the binding rule, not the model

Under the first prompt, the residue is 157 errors still standing after correction on education, and 108 of them (69%) have one shape: the dominant residual shape. The sentence names the pupil and then the class, and linear carry-forward binds the pupil's facts to the class — the data is right, the English is right, and the verifier reports a field the class does not have. It touched 17 of the 35 non-converged query-runs. Wrong values are 40; the rest is small and mixed.

Told the rule, the models follow it

The second prompt adds two sentences: a fact may name its own record when a sentence names two subjects, and a cutoff from the question is not a fact. Nothing else changes. On finance, Claude Opus 5 verifies 100% of claims on the first pass in every run — every claim, first pass, every run — and so do Claude Sonnet 5 (100%, every claim, first pass, every run) and DeepSeek V4 Pro (100%, every claim, first pass, every run). On education, Claude Sonnet 5 rises to 99.4%, DeepSeek V4 Pro to 99.2% first pass and 100% after one correction, and Claude Opus 5 to 95.4% — two of its three runs verify everything on the first pass, and in the third it reverted to the very phrasing the rule addresses, which is the honest cost of a rule a model must follow rather than a constraint it cannot break. The 108 binding errors of the first prompt become 16 under the second.

view this page's raw ProveML markup

<h2>What the verifier itself catches</h2>
<p>Before measuring any model, the paper measures the instrument. @[study:detection]{the detection study} planted %[injected]{20} deliberate errors in otherwise valid markup — wrong values, wrong entities, missing context, subtle canonicalization slips — and the verifier caught %[detected]{20} of them: ?[all: DETECTED_EVERYTHING]{nothing slipped through}. That is a conformance test, not a benchmark; exact comparison either sees a difference or there is none.</p>

<h2>The mechanism is within reach of frontier models</h2>
<p>Three models that were frontier in August 2026 — Claude Opus 5, Claude Sonnet 5, and the open-weight DeepSeek V4 Pro — over two benchmarks, three runs each: @[study:frontier]{the frontier study}. Across all its %[queryRuns]{342} query-runs, %[empties]{0} answers came back empty or without markup: ?[ne: NOTHING_EMPTY]{no empty answers at all}. @[model:opus5]{Claude Opus 5} opens at %[eduFirst]{86.5}% first-pass verification on education (spread %[eduFirstSd]{0.3}) and one correction pass lifts it to %[eduFinal]{94.8}%; @[model:deepseek]{DeepSeek V4 Pro} reaches %[finFirst]{100}% on finance on the first pass and covers %[finCover]{96.4}% of its numbers, the strongest of the three.</p>

<h2>What remains is the binding rule, not the model</h2>
<p>Under the first prompt, @[residue:frontier]{the residue} is %[total]{157} errors still standing after correction on education, and %[binding]{108} of them (%[bindingPct]{69}%) have one shape: ?[bd: BINDING_DOMINANT]{the dominant residual shape}. The sentence names the pupil and then the class, and linear carry-forward binds the pupil's facts to the class — the data is right, the English is right, and the verifier reports a field the class does not have. It touched %[bindingQueryRuns]{17} of the %[nonConverged]{35} non-converged query-runs. Wrong values are %[wrongValue]{40}; the rest is small and mixed.</p>

<h2>Told the rule, the models follow it</h2>
<p>The second prompt adds two sentences: a fact may name its own record when a sentence names two subjects, and a cutoff from the question is not a fact. Nothing else changes. On finance, @[model:opus5]{Claude Opus 5} verifies %[fin2First]{100}% of claims on the first pass in every run — ?[c1: CLOSED_FIRST_PASS]{every claim, first pass, every run} — and so do @[model:sonnet5]{Claude Sonnet 5} (%[fin2First]{100}%, ?[c2: CLOSED_FIRST_PASS]{every claim, first pass, every run}) and @[model:deepseek]{DeepSeek V4 Pro} (%[fin2First]{100}%, ?[c3: CLOSED_FIRST_PASS]{every claim, first pass, every run}). On education, @[model:sonnet5]{Claude Sonnet 5} rises to %[edu2First]{99.4}%, @[model:deepseek]{DeepSeek V4 Pro} to %[edu2First]{99.2}% first pass and %[edu2Final]{100}% after one correction, and @[model:opus5]{Claude Opus 5} to %[edu2First]{95.4}% — two of its three runs verify everything on the first pass, and in the third it reverted to the very phrasing the rule addresses, which is the honest cost of a rule a model must follow rather than a constraint it cannot break. The %[residue:frontier.binding]{108} binding errors of the first prompt become %[residue:frontier2.binding]{16} under the second.</p>

the paper (pdf, 16 pages) → · benchmarks & run artifacts → · what ProveML is →