A computer-assisted proof rests on a checker, and a checker that has never been seen failing proves nothing about its own attention. The proposal here is one sentence: publish, beside every computational certificate, the mutation that makes its checker go red — the minimal semantic corruption of the certified object, the clean run’s zero exit, the corrupted run’s nonzero exit, and the hashes of what was run. This page states the proposal, credits the prior art it is built from, reports the audit incident that shows what its absence costs, and points at working examples — every one of them on this site, checkable now.
The idea is old, and it is not mine. A checker that exits zero on every input has passed every certificate ever written; so some demonstration that it can exit nonzero is logically prior to reading anything into a green result. Software engineering made this a discipline in 1978 — mutation testing: seed a small deliberate fault, and a test suite that fails to notice is measured by that miss (DeMillo, Lipton & Sayward, Hints on Test Data Selection: Help for the Practicing Programmer, Computer 11(4):34–41, 1978, DOI 10.1109/C-M.1978.218136). Experimental science has owned the same idea longer under a different name: an assay earns its readings by passing a positive and a negative control. Nothing in this note claims that mechanism as new. The claim is narrower and about publishing practice: in the computer-assisted-proof genre, the control is run privately or not at all, and almost never ships — of six computer-assisted-proof artifact repositories opened for this note, four ship no tests of any kind.
The strongest published relative is twenty-six years old and comes from scientific computing. In Sandia report SAND2000-1444 (Salari & Knupp, Code Verification by the Method of Manufactured Solutions, June 2000, DOI 10.2172/759450), one author took the Navier–Stokes code the report had just verified to second order and deliberately sabotaged it, blind, twenty times across twenty-one cases — the twenty-first, by design, contained no mistake at all. The other author then had to find the faults using the verification procedure itself. Their §7 reports the outcome with a candour worth imitating: all ten order-of-accuracy mistakes were caught, the static and divergence mistakes were caught, the efficiency mistake and seven formal mistakes were not — and none of the escapes affected whether the equations were solved correctly. A seeded blind protocol, a placebo, and an honestly stated detection scope, in 2000.
Mutation has reached proof artifacts too. Mutation Analysis for Coq (Celik, Palmskog, Parovic, Gallego Arias & Gligoric, ASE 2019, pp. 539–551, DOI 10.1109/ASE.2019.00057, with the mCoq tool demo) mutates Coq definitions and asks whether a project’s proofs notice; Using Mutations to Analyze Formal Specifications (DOI 10.1145/3563768.3563960, 2022) and Mutation Testing Based Evaluation of Formal Verification Tools (DOI 10.1109/DSA.2017.10, 2017) carry the same operator into specification and tool evaluation — both cited here by title, their identifiers verified and their bodies unread.
And where a verified checker exists, the question “can it go red?” is answered by something stronger than a test: a soundness theorem about the checker itself. The SAT world has this — machine-checked certificate checkers proved correct down to machine code (Tan, Heule & Myreen, cake_lpr: Verified Propagation Redundancy Checking in CakeML, TACAS 2021, pp. 223–241, DOI 10.1007/978-3-030-72013-1_12; Lammich, Efficient Verified (UN)SAT Certificate Checking, J. Automated Reasoning 64(3):513–532, DOI 10.1007/s10817-019-09525-z). That is the right answer where it exists. To our knowledge, none of the pipelines that carry computer-assisted proofs in analysis — CAPD, INTLAB, Arb, the bespoke MATLAB and Julia archives that accompany the papers — has a verified checker of that kind. In exactly that gap, the empirical falsifier is the instrument that is available today, to every author, at the cost of one patch and two runs.
On 13 August 2026, Fan Zheng posted the audit that makes the gap concrete (Computer-assisted Proof Under Audit: Typos, Certificate Errors, and Reproducible Exact Checks for a Symbolic Invertibility Proof, arXiv:2608.13067): a version-pinned, source-level audit of the exact-arithmetic certificate accompanying arXiv:2310.19781v2 and its 2025 Communications in Mathematical Physics version. The audit reports 11 proof-affecting defects, alongside typographical slips, with reproducible exact counterexamples to several implemented bounds. Zheng states the priority claim as his own — the first such audit, to his knowledge — and his conclusion draws exactly the line this note cares about, quoted verbatim:
“The findings do not refute the intended theorem or its analytic reduction, but they show that the published certificate does not prove the claimed conclusion.”
The theorem may well stand; the certificate — the artifact whose entire purpose was to remove doubt — did not do its job, and it took an independent auditor, after journal publication, to notice — the journal version corrects none of the audited items, as Zheng’s abstract states plainly. A shipped falsifier would not have caught every one of those defects either — no single instrument would — but it would have established the one thing now in doubt at the base of the stack: that the checker, as released, was ever capable of rejecting anything.
What shipping a falsifier means, in the form this site has converged on:
This is not hypothetical practice. Measured on 14 August 2026: all seven single-file lane verifiers published beside this site’s reports end with mutation controls that must fire — the air-taxi corridor verifier ends by showing its uniqueness condition failing at zero price and conservation going red under a one-unit corruption; the Maxwell-counterexample verifier carries the same pattern, the Poisson verifier ends with its two controls as literally its last lines, and the certificate taxonomy states what each verdict does and does not establish. Behind the pages, the internal evidence ledger held, same date, fifteen claims carrying seventeen recorded mutation reds — each a patch with both exit codes and file hashes, produced by a tool whose own header forbids a bypass flag. Measured against today’s tree by the deriving gate’s own predicate, eleven of the seventeen, across eight claims, are fresh — the recorded target still hashes to the bytes the red was proven against — and six have rotted as targets moved or were retired. That rot is exactly the failure mode the fourth bullet names, and it is disclosed here rather than skipped, with the re-authoring owed: the rule would be worth nothing if it exempted the page that proposes it. Dated records, not live readouts; the linked pages carry the live checks.
One boundary drawn honestly, because the community’s own tooling is moving.
On 3 August 2026, the RadiiPolynomial.jl toolkit’s
v0.11 added genuine negative-path tests: its existence checker is exercised on
hand-constructed infeasible bounds, with a paired accept/reject control and an
asserted failure message (test/rpa/interval_existence.jl). That is
checker-level negative control inside a library’s unit suite — a
real step, eleven days before this note, and exactly the direction this proposal
points. The remaining step is the one this page argues for: the same discipline
attached to each published certificate, as part of what the paper ships.
The mechanism is not new and is not claimed: it is mutation testing (1978), blind seeded verification with a placebo (2000), and mutation analysis for proof artifacts (2019), credited above. We are not aware of any published computer-assisted proof that ships a mutation-verified falsifier beside its certificate — a documented search, not a proof: eleven literal queries and six successful source fetches on 14 August 2026, plus six CAP artifact repositories cloned and read — four of which ship no tests of any kind — and no sweep of MathSciNet, zbMATH, Scopus, or full-text indices. One repository with a seeded-mutant test beside a published certificate, found by anyone, falsifies the negative; corrections are wanted and are published in the errata. This is a proposal, not a standard: one tree practices it. And an audit is not the practice proposed here — Zheng’s work is external and after publication; the falsifier belongs to the author, at publication, which is precisely why it cannot be vacuous reassurance: it ships with the artifact it indicts.