One person, a fleet of AI agents, and a discipline built on the assumption that both will be wrong: no check counts until it has been seen failing on a deliberately broken copy, every agent has a way to report failure that is scored as success, and the errors that get through anyway are published, dated, in the open. Everything else on this site is output; this page is the method. It is written as an essay, but every incident in it is a dated record.
The division of labour is stated on the about page and repeated here because it is the premise of everything that follows: the mathematics, the design of every check, and every decision about what may be claimed are mine. The writing and much of the implementation are done by AI agents — coding agents run under standing instructions, dispatched in parallel, their outputs landing as drafts in an append-only internal record. The output rate of this site is a consequence of that arrangement.
What makes the arrangement trustworthy is not trust. An agent’s output is treated exactly like a numerical claim from a stranger: it enters as a claim, and it becomes a result only when a check passes — a check that has itself been checked, in the sense of the next section. The same standard applies in the other direction, to me: my own drafts go through the same falsifiers, and most of the entries in the public errata are my errors, found by me, after publishing. The discipline is symmetric because the failure it guards against is symmetric — a human who wants the green light and a model that wants to please converge on the same defect.
A test that has never failed is consistent with correct code, and equally consistent with a test that tests nothing. So the unit of verification here is not the check but the check plus the demonstration that it can go red — in the right direction. Every falsifier is run twice, in a throwaway copy of the tree: once against a deliberately broken kernel, where it must exit nonzero, and once against the clean tree, where it must exit zero. A falsifier that passes the broken copy has no teeth; one that fails the clean tree is not strict, it is broken. Only the pair counts, and the tool that proves the pair has no bypass flag — its own header says there must never be one, because a mutation patch that no longer applies is a failure to be re-authored, never a step to be skipped.
Two further rules exist because they were paid for. A skip is never a pass, and a crash is never a verdict: a check that could not run reports that distinctly, because a runner that died before its first assertion looks exactly like a runner with nothing to report. And counts are measured, never remembered: any number, line count, or citation that ships is re-measured in the session that ships it, a rule bought by, among other things, a modulus written from memory as prime that was composite. The standing instructions the agents run under state each rule together with the incident that paid for it — a rule with no receipt gets optimised away by the next rewrite.
The deepest failure mode is the one the rules above do not reach: passing and being checked are independent properties. A check that can go red, and that is green, may still be looking at almost nothing. The model-checking literature has a name for the limit case — a specification satisfied vacuously (Beer, Ben-David, Eisner & Rodeh, Efficient Detection of Vacuity in Temporal Model Checking, Formal Methods in System Design 18(2), 2001, DOI 10.1023/A:1008779610539) — and the term is used here rather than a local invention.
It is not hypothetical in this tree; it is measured. On 9 August 2026, across thirteen of the internal gates: deleting a slice of what a check reads — twelve of twelve noticed. Narrowing the sweep, with the tree untouched — four of eight stayed green after losing 76–82% of what they swept. One gate verified five of its twenty-one pinned artifacts and printed “every byte every cert names is the byte on disk.” Deletion and narrowing are different failures, and a red control only proves a check notices a wrong value — it says nothing about whether the check was pointed at the right amount of work.
So there is a probe for it: it narrows what each check reads, re-runs the check, and asks whether the verdict moved. A first full sweep on 10 August 2026 found six gates blind and all six were repaired the same day; one of them was blind again a day later, un-done by an unrelated improvement. That recurrence is the honest finding: blindness is not a bug you fix once, it is a property that decays under change, which is why an instrument exists rather than a checklist. And the limit of the practice, stated plainly: no gate runs the probe automatically. The newest entry in the errata — open since 6 August 2026 — is a real fix that an unrelated improvement silently reverted, found only by running the instrument by hand. It stays open on the log until it closes.
The agent fleet is organised as named roles — fifteen of them as of 13 August 2026 — and the doctrine for running them reduces to three principles, each bought by a measured incident.
test in every required field, and two of them labelled the
result CLEAR — a fabricated reassurance, not a missing one. So every role carries
an explicit failure vocabulary that is scored as a success — UNCERTAIN,
REFUSED, UNREACHABLE, no-law-found — with a reserved slot in its required output,
and the consumer of any agent’s output applies a mechanical screen the producer
never applies to itself: a junk-token list, minimum lengths on evidence fields, no
citation without a resolvable identifier, no claimed search without its numbered literal
queries, and every hash recomputed by the reader.Around the roles sits the record: the sessions’ working files — 86 of them as of 13 August 2026 — and a failure catalogue of 25 dated entries, both append-only. A record of what happened is never edited to match what happened next; a superseded plan is superseded in writing. The internal evidence ledger, same date, holds 14 claims, 14 measurement runs, 68 attack records and 3 certificates; what ships publicly from each claim is the part that makes it checkable — the page, its program, and its falsifier.
The tempo is the visible consequence, and it has dates. The Maxwell-conjecture counterexample paper appeared on 29 July 2026; its 24 equilibria were certified here, with published falsifiers, on 4 August. The preregistered audit of my own verifier committed its predictions before the harness existed, was falsified at 9 of 14 by its own instrument, and published the falsified prediction as the headline — then hardened the verifier the same day and re-measured at 14 of 14. The point of the discipline is not that it prevents error; the errata above proves it does not. The point is that the cost of being wrong is a page, not a retraction of trust — because nothing was ever asked to be taken on trust.
This way of working is young, but it is no longer only here. In July 2026 Joseph K.
Miller published A Formalization of the
Mean-Field Derivation of the Vlasov Equation (arXiv:2607.08986): one mathematician
directing coding agents to formalize Dobrushin’s mean-field theory in Lean 4
— existence, uniqueness, stability, the mean-field limit — with a falsifiable
win condition (the development compiles with no sorry, on the
library’s foundational axioms alone), headline theorems in about a week, and the
per-session agent logs recoverable from the public repository. The detail that belongs on
this page: the one defect he singles out was a vacuous pass. A top exponent in the
library’s differentiability class meant real-analytic where smooth was
intended; a nonzero real-analytic function cannot have compact support; so the class of
test functions had quietly collapsed to zero and a hypothesis held vacuously. The
machine’s proof was valid, and empty — the human caught it by reading.
Same division of labour, same failure mode, different proof stack. There, a formal kernel checks every step and the human guards the statements. Here there is no kernel, so the statements are guarded the way this page describes — falsifiers that must be shown to fail, and a probe for the checks that pass while looking at nothing. The two stacks meet at the same lesson: the machine can certify that the proof is airtight; it is much worse at noticing that the theorem has become empty.
Checkable is not correct, and this page claims the weaker property only. The checks and the code share one author, so they rule out slips but not a shared misconception. The agent transcripts and the internal records described above are working files, not public artifacts; what is public is what makes the results checkable — the programs, the falsifiers, the certificate taxonomy that says exactly what each verdict does and does not establish, and the errata. Nothing here is peer-reviewed, and no result on this site has yet been independently reproduced — which is why every page ships its falsifier rather than asking for trust.