AI with Authority

Chapter 1: Five Artifacts, One Shape

Strip away the fleet, the silicon, and the number theory, and the Salt method is one repeated gesture. The human prompts an agent in English. The agent returns five things. Always the same five, at every scale — from the design of the whole project down to the design of a single component. This chapter builds each of the five, shows what travels between agents, and lands on the artifact the paper says deserves the most emphasis — the one most engineers have never heard of.

Trust has two hard halves

Start from the problem the five artifacts exist to solve. The paper opens its methodology section with a symmetry most treatments of verification skip.

The familiar half: the implementation is hard to read. Code is dense, stateful, and full of edge cases; a human reviewer misses things. Machine-checked proof addresses exactly that — if the kernel accepts a proof that the implementation meets the specification, no human ever needs to re-derive it.

The less familiar half: the specification is also hard to read. A formal statement is written in the same unforgiving logic as the proof. And here is the trap that swallows naive verification projects: a proof is only as good as the statement it proves. A kernel will happily certify a vacuous theorem, a theorem about the wrong function, or a theorem whose hypotheses quietly exclude every interesting case. The kernel checks the arrow from statement to proof; it has no opinion about whether the statement is worth proving.

The five artifacts, one by one

Every prompt, at every level, returns this bundle. The paper’s notation (from its Figure 2) is compact enough to memorize:

Notice what the turnstile appears on: the proof and the certificate. The kernel checks twice — once for the implementation’s correctness (P meets S), once for the specification’s comprehensibility (S entails S′). That double duty is the paper’s Figure 2 in one sentence.

The certificate — why the implication direction is everything

The certificate deserves the slow walk, because the paper singles it out: the last artifact deserves emphasis.

The problem: a real specification S might be three screens of quantifiers, index arithmetic, and library vocabulary. The human must decide whether S is the statement they wanted — that is the one duty that remains human — but three screens of quantifiers is exactly the reading load the method promised to remove.

The move: the agent also produces S′ — the same claim restated in a smaller, plainer vocabulary — together with a kernel-checked proof of the implication S ⇒ S′. The contract is precisely that implication, and its direction is the entire trick.

Think it through with a toy example (ours, not the paper’s — the mechanism is the paper’s). Suppose the fleet proves S = “the output list is a sorted permutation of the input.” A certificate might restate S′ = “the output list is sorted.” S′ is weaker: it drops the permutation clause. A reader of S′ therefore underestimates what was proved — they credit the system with less than it earned. Now flip it: could a certificate ever say S′ = “the output is a sorted permutation and runs in linear time” when only sortedness was proved? No — because S ⇒ S′ would then be false, and the kernel would reject the certificate’s own proof.

And the certificate has a form every working engineer already knows. Its most familiar shape, the paper says, is a test. A test is a tiny, concrete, readable claim: “on this input, the system produces that output.” If your proved specification implies the test’s claim, then the test is a certificate — a restatement in the simplest vocabulary there is, single instances. For the working engineer the experience is routine: write tests as always, with one extra operation — promoting a test to a theorem. The spine you will meet in Chapter 5 does exactly this: its per-round kernel fixtures — concrete input/output checks of the application, proved in the kernel — are promotions of ordinary tests.

What actually travels between agents

Here is the Concept-plus-Realization view — the data flow, not the philosophy. In a naive multi-agent system, agents exchange prose: “I proved the lemma, here’s a summary.” Prose between agents compounds error — each hop is a chance to hallucinate, drop a hypothesis, or inflate a scope. In the Salt configuration, mathematical claims travel between agents only as kernel-checked artifacts: the actual Lean object, checkable by the recipient in one command, axioms auditable per theorem. An agent that receives a claim does not trust the sender’s account of it; it re-checks. The bus carries assertions with their evidence attached, and the evidence is machine-verifiable at every hop.

The bundle, walked end to end on a toy

Abstract bundles slide off the mind, so here is one at the smallest possible scale — the example is ours (the paper’s own instances are the spine’s components, which need Chapter 5’s machinery); the shape is exactly the paper’s. Objective, in English: “give me a function that finds the largest element of a list of numbers.” The agent returns:

-- P, the implementation
def largest : List Int → Option Int := …

-- S, the specification (written before P, per the elicitation)
theorem spec : ∀ xs, xs ≠ [] →
  ∃ m, largest xs = some m ∧ m ∈ xs ∧ ∀ x ∈ xs, x ≤ m

-- the proof: kernel-checked, so it travels as an artifact
⊢ largest ∈ spec        -- checked by the Lean 4 kernel

-- T(P), adversarial tests: controls that MUST be able to fail
#eval largest []            -- boundary: none, and the spec excludes it
mutate (largest → head) ⇒ spec proof breaks   -- the bite check

-- S′, the certificate, with its kernel-checked implication
theorem cert : largest [3,1,2] = some 3     -- a test, promoted
⊢ spec ⇒ cert

Read the bundle the way the human would. They never open P. They read S′ — one line, one concrete instance — and if they want more, they interrogate: unfold spec’s binders (what does the quantifier range over? lists of what?); justify the hypothesis (why xs ≠ []? what does the function do on empty input, and is that what I wanted?); produce a variant (prove it again for the version returning an index). Each answer comes back kernel-checked. The empty-list hypothesis is exactly the kind of thing this interrogation surfaces: the spec as written says nothing about empty input — a scoping choice the human must notice and either accept or send back. No kernel will flag it, because it is not an error; it is a decision. That is what “human attention reserved for statements” means in practice.

Notice the division of labor the table makes visible: the kernel appears twice, the human once — at the single artifact designed for human eyes. Every arrow that could carry a hallucination between agents passes through a checker first. That is the “wire format” view of the method: the bus protocol simply has no message type for an unchecked mathematical claim.

Adversarial tests — checking that the proof has bite

Why does a bundle that already contains a kernel-checked proof still contain tests? Because of the statement-half of the trust problem again, in a subtler costume.

Imagine a theorem that is true, kernel-checked… and toothless. Perhaps its hypotheses are unsatisfiable, so it holds vacuously. Perhaps it constrains a code path the implementation never takes. The kernel cannot flag toothlessness — a vacuous truth is still a truth. So the bundle carries adversarial controls: tests constructed to fail if the proof’s protection is real. Break the implementation in the way the theorem forbids — does the control catch it? If a control cannot be made to fail under any mutation, the control is decoration, and the method’s rule is blunt: every control must be able to fail.

This is the method’s second commitment surfacing at the artifact level. The paper states three commitments concisely, and they organize everything you will see later:

The certificate ladder — one theorem, many readers

Because a certificate is just an implied restatement, nothing limits a theorem to one. A single proved specification can carry a ladder of certificates at different grains — each rung kernel-checked against the rung above (the ladder image is ours; the contract making it sound is the paper’s):

Implication composes, so the guarantee survives the whole descent: if S holds and every rung is kernel-checked, every rung holds — and every rung can only understate. This is why the paper can say the certificate layer makes statement-level review tractable rather than merely possible: review happens at whichever rung the reviewer can actually read, with no loss of soundness for descending.

Review as active interrogation

One more piece completes the shape, and it corrects a natural misreading. The certificate is the entry point to comprehension, not its end. Reading S′ is not the whole review; the method’s review is active interrogation.

The human questions the system, and the system answers with kernel-checked evidence — three concrete moves the paper names: unfolding a statement’s binders (expanding the quantifiers and definitions to see what the symbols actually range over); justifying a hypothesis (why is this assumption here? what breaks without it?); and producing a variant under a changed assumption (prove it again with the boundary case included — or show me the counterexample). Each answer is itself checkable; the conversation never degrades into taking the model’s word.

The paper adds a quietly important empirical note: the author works this way daily, and the campaign registers are substantially a transcript of this interrogation. And because the artifacts are public, a referee can do the same with the public artifact — the review interface the author used is the review interface the reader gets.

To make the moves concrete, here is a sixty-second interrogation — the dialogue is ours; each move is one of the paper’s three, and each answer’s crucial property is that it arrives kernel-checked. The certificate on the table: “the executive never schedules two tasks in the same slot.”

Move 1 — unfold the binders. “What does ‘slot’ range over?” The system expands the definition: slots are entries of the schedule table, indexed by tick. The human now knows the theorem is about the table, not about wall-clock time — a distinction that matters if an interrupt can fire between ticks. The unfolding is definitional, so the kernel vouches for it.

Move 2 — justify a hypothesis. “The statement assumes the task count is at most the table size. Why?” The system produces the failing case: with more tasks than slots, no injective assignment exists — and, if asked, a kernel-checked lemma that the bound is necessary. The hypothesis is now understood as load-bearing, not decorative.

Move 3 — vary the assumption. “Prove it again with dynamic task creation enabled.” The system either returns the variant theorem, kernel-checked — or returns a counterexample showing the property genuinely fails there, which is not an error but a discovery: the specification’s boundary, located precisely. Either answer advances the review; neither requires trusting anyone’s prose.

Multiply this by five weeks of daily practice and you have the paper’s claim that the registers are “substantially a transcript” of interrogation: review, in this method, is not a reading posture. It is an experimental science whose instrument is the kernel.

Why five — the failure each artifact kills

The bundle’s size is not arbitrary. Delete any one artifact and a specific, historically observed failure walks in through the gap:

Five artifacts, five failure classes, each plugged by construction. The paper’s claim that this shape recurs at every scale is therefore a claim about failure classes recurring at every scale — which anyone who has watched a project die of an unenforced architecture document can confirm from the field.

One shape at every scale

The five artifacts are not just for functions. The method’s first required invariant (R1, formally stated in Chapter 3) demands the bundle at every level from project design to component design. A project plan has an implementation (the plan), a specification (its objectives), a proof obligation (its acceptance criteria), adversarial tests (the refuter pass that attacks it), and certificates (the summary the human actually rules on). The gesture is fractal — which is why the method scales down to a lemma and up to a tapeout without changing shape.

And notice, finally, that the paper you are reading is itself shaped like its own bundle — the recursion is deliberate, and seeing it will organize the whole second half of this lesson. The implementation is the campaign: the corpus, the stack, the die. The specification is the pre-registered objectives and acceptance criteria the elicitation discipline produced. The proof is the replayable record: kernel-checked theorems, commit-verified provenance. The adversarial tests are the refuter passes, the witness checks, and the final-morning priority survey that attacked the paper’s own claims. And the certificates are the paper’s stated summaries — each number with its scope sentence, each claim at its grade — written so a reader can only underestimate what the record supports, never overestimate it. R1 said the five artifacts appear at every level, from component to project. The project’s topmost level is the publication itself, and the shape holds there too.

Exercises

1. Certify by hand. Take S = “for every non-empty input list, the function returns the maximum element in O(n) comparisons.” Write two valid certificates (weaker restatements) and one invalid certificate (a restatement not implied by S), and say which clause of the contract the invalid one violates. Check: “returns an element of the list” and “on [3,1,2] returns 3” are valid (each implied by S); “runs in O(1) space” is invalid — S says nothing about space, so ⊢ S⇒S′ has no proof and the kernel rejects it.

2. Give a proof teeth. You have a kernel-checked theorem: “the scheduler never runs two tasks in the same slot.” Design one adversarial control that would fail if the theorem’s protection were fake (say, the theorem accidentally quantifies over an empty set of slots). Check: a mutation test — patch the scheduler to double-book deliberately, then confirm the control (and the proof) actually break. If nothing breaks, your theorem was about nothing.

3. Spot the artifact. Your CI pipeline has: unit tests, a README, type signatures, code review comments, and a changelog. Map each onto the closest Salt artifact (or note that it has none) — and identify which Salt artifact your pipeline entirely lacks. Check: tests → T(P) (usually without adversarial controls); type signatures → a very weak S; README → an unchecked S′ — a certificate with no ⊢, which is exactly the gap: nothing in a normal pipeline proves the docs are implied by the code’s actual guarantees.

Chapter 2: The Incorruptible Referee

Everything in the last chapter leaned on one load-bearing phrase: kernel-checked. This chapter opens the kernel up. What exactly is this referee? Why can no hallucinated proof pass it? What, precisely, does trusting it commit you to? And — the question the paper treats with unusual honesty — what are the two places the referee structurally cannot see, and what does the method do about them?

What a proof kernel is

Inside a modern proof assistant like Lean 4 there are really two programs wearing one trench coat.

The outer program is enormous and friendly: parsers, tactics, automation, libraries, editors — hundreds of thousands of lines whose job is to help you construct proofs. It is allowed to be buggy, because nothing depends on trusting it.

The inner program is the kernel: a compact, independent checker whose only job is to take a fully elaborated proof term and verify, step by mechanical step, that it derives its statement from the axioms. Every proof, no matter which clever tactic produced it, is re-checked by the kernel before it counts. This architecture has a name and a lineage the paper cites: the LCF tradition (after the 1970s theorem prover that invented the pattern), and the design test it satisfies is the de Bruijn criterion — a system meets it when its proofs can be re-verified by a small, simple, independent checker, so that trust rests on that checker alone.

In the Salt workflow the kernel’s position is absolute: every mathematical claim in the work is checked by the Lean 4 kernel against mathlib — the community’s mathematical library, version-pinned in the paper’s Methods — and the kernel is the sole arbiter of mathematical truth in the workflow: no proof is reviewed by the human, ever. Read that sentence again, because most people refuse it on first contact. Not “proofs are spot-checked.” Not “important proofs get a second look.” No proof is reviewed by the human, ever. The entire review budget moves elsewhere — and the rest of this chapter is about where it goes.

The axiom audit — checking what the kernel assumed

A kernel verifies that a proof follows from the axioms. So the honest question is: which axioms?

If a development quietly adds a convenient axiom — “assume the following lemma” — the kernel will faithfully check everything downstream, and the whole edifice is worth nothing. The campaign closes this hole with per-theorem axiom audits: for every registered theorem, the exact axioms it depends on are extracted and checked against a whitelist. The paper’s policy, stated in full: the three standard axioms only, no custom axioms, and no native_decide. (The paper does not name the trio; in Lean’s formulation the three standard axioms are propositional extensionality, quotient soundness, and choice — that identification is ours, standard Lean background rather than the paper’s text.)

That last exclusion is worth a sentence, because it shows how fine-grained the trust accounting is. native_decide is a Lean facility that proves a statement by compiling it to native code and running it — fast, and usually fine. But it enlarges the trusted base from “the kernel” to “the kernel, plus the compiler, plus the runtime that executed the check.” The campaign refuses the enlargement: if the kernel didn’t check it, it isn’t checked. A trust base is like a ship’s waterline — it is defined by its lowest point, not its average.

The referee’s economics — why checking is the cheap half

Chapter 0 claimed the inversion; here is its mechanical core, visible now that you know what the kernel does. Producing a proof is search — the agent explores a space of tactics, lemmas, and reformulations, and search is expensive: that is where the fleet’s tokens go. Checking a finished proof is not search; it is a single deterministic pass of a small type-checker — seconds of compute, flat cost, no model in the loop. So the workflow’s expensive step (generation) is exactly the step AI just made cheap and parallel, and the workflow’s trust step (checking) was always cheap — it merely used to be preceded by the truly expensive step, a human writing the proof. Remove the human from proof-writing and the old cost structure collapses: what remains is cheap generation, cheap checking, and a human budget spent entirely on the two uncheckable ends.

Put numbers on the human end, using the register counts you will meet later — the division is ours, the counts the paper’s. The record registers 73 headline theorems over a 37-day campaign: about two per day. Two statements a day is a readable load for one person — through certificates, under interrogation — even while the fleet behind them lands 56 commits a day. That 28-to-1 ratio between commit tempo and statement tempo is the inversion as lived experience: the kernel absorbs the tempo; the human reads the meaning. Sixty years of verification economics assumed one person must do both. Splitting them is the whole trick, and only an incorruptible checker permits the split — with a corruptible one, the human must audit the auditor, and the tempo crushes them again.

The two ends the referee cannot check

Here is the part of the paper that separates it from every breathless formal-methods pitch you have read. The referee has two ends it structurally cannot check, and the method is explicit about both.

At the back: the certificate layer. The kernel can check that S implies S′. It cannot check whether S′ means to its reader what the reader thinks it means. Meaning lives in a human head; no turnstile reaches there. Chapter 1’s one-way mirror bounds the damage — misreading a certificate can only underestimate — but reading remains a human act.

At the front: the specification itself. This is the accusation verification has always faced, and the paper names it head-on: verification is most often accused of merely relocating the problem — you still have to trust that the formal specification captures what the human actually wants. That correspondence — between intent in a mind and text in a logic — lives in the human alone. No machine can check it, because the machine has access to only one side of the correspondence.

What do you do with a gap no machine can close? The method’s answer: you work it as a discipline rather than an assumption. The paper gives the elicitation pipeline in full, and it deserves the walk because it is the least automatable, most transferable part of the whole method:

The paper compresses the philosophy of that pipeline into one aphorism worth engraving: a specification written after the code is a description; written before, it is a requirement. And it notes, for provenance, that this elicitation practice predates the campaign, coming from the author’s prior collaboration with agents.

Elicitation, dramatized — sixty seconds of the front end

To make the front-end discipline concrete, here is a compressed dramatization — the dialogue is ours; every move in it is a named step of the paper’s pipeline. The human’s opening objective: “I want the executive to guarantee tasks can’t interfere with each other.”

Two properties of this exchange deserve names. First, the agent’s questions are cheap and the human’s answers are load-bearing — the exact inversion of the usual AI workflow, where the human labors over prompts and the model’s output is disposable. Elicitation treats human intent as the scarce signal to be extracted carefully, once, and frozen. Second, the “negative space” axis produces the requirement most specs silently lack: a statement of what is deliberately not promised. Chapter 3’s R6 gives that statement formal standing — out-of-domain hypotheses, named in the theorem itself.

The three standard axioms — what “standard” buys

One more layer of precision on the audit, because “three standard axioms” is doing quiet work. (What follows is Lean background, ours — the paper says only “the three standard axioms.”) Lean’s mathlib development rests on three classical axioms — propositional extensionality, quotient soundness, and choice — which together give you ordinary classical mathematics as a working mathematician practices it. The point of auditing per theorem is not suspicion of these three; it is that the audit makes the dependency set an checkable fact rather than an assumption. A theorem’s axiom list is printed by a command; the whitelist comparison is mechanical; a fourth axiom — however innocent-looking — fails the audit loudly. The campaign’s configuration accepts exactly mathlib’s classical baseline and nothing else, and can prove it accepts nothing else, one theorem at a time.

Watch the counters as you play: the attempted column climbs freely — hallucinated proofs cost the fleet nothing but budget — while the record column admits only what survived every gate, and the incorrect-in-record counter is not low; it is structural zero. That is the abstract’s central sentence rendered as a game: you cannot make the third counter move, no matter which button you press or how often. The gate does not get tired, does not extend credit to fluent submissions, and does not have a bad day — and the fleet’s entire operating tempo is built on those three absences.

Play the fourth button several times, because it teaches the chapter’s deepest lesson. The kernel gate is perfect at its job and blind outside it: a true theorem about the wrong thing sails through checking and audit. The only thing standing between that artifact and the record is the human reading the statement — through its certificate, under interrogation. That is why the method spends its entire human budget there, and why the error ledger you will meet in Chapter 4 is full of statement-level catches, not proof-level ones.

“Did it check” — the mechanics of replay

The first of the two review questions deserves its mechanics spelled out, because they explain a phrase from the abstract that sounds like marketing and is actually an operation: every mathematical claim is kernel-checked and replayable.

Replayable means: you, the reader, clone the public repository, run one command, and your machine’s kernel re-checks the entire development from source — every proof re-derived, every axiom re-audited, on hardware the authors never touched. The paper’s data-availability statement says it flatly: every theorem replays with one command. Contrast this with the two familiar alternatives. Reproducing an empirical paper means re-running experiments for weeks and hoping the environment matches. Checking a traditional mathematics paper means finding three qualified referees and months of their attention. Replaying a kernel-checked corpus is minutes of compute and zero trust in the authors — the verification travels with the artifact.

This is also why the fleet can be fast without being reckless. An agent’s half-finished, wrong, or hallucinated proof attempts cost nothing but its own budget: they fail to check, privately, and are never seen again. Only checked artifacts propagate. In an unverified workflow, speed multiplies error; behind a kernel, speed multiplies only attempts — and attempts are cheap while errors are not. That asymmetry is the economic engine of the whole paper, stated small.

What “incorruptible” does and does not promise

Precision cuts both ways, so state the referee’s own trust base honestly — the paper’s phrase is that the trust base is deliberately small, not zero. Trusting a kernel-checked theorem means trusting: the kernel implementation itself (small, stable, scrutinized by an entire community for years — and independent of everything that generates proofs); the three standard axioms; and the statement as written. That is the whole list. Compare it to what you are not trusting: not the tactic framework, not mathlib’s proofs (the kernel re-checked those too), not the agent, not the model family, not the prompt, not the person who ran it. The de Bruijn criterion is exactly the engineering that makes the list this short — and the reason the same guarantee holds for a proof produced by a student, a sieve expert, or a language model having a very strange day.

What incorruptibility does not promise, and the paper never claims: that the work is meaningful, novel, or well-scoped. The kernel is a perfect referee for exactly one game — derivability. Every other game played in the campaign — measurement, priority, design quality — gets a different referee, and Chapter 3’s R2 is the rule that no game may be played without one.

Notice the design logic of the table: referees are ordered by corruptibility, and the method assigns each claim to the least corruptible referee that can judge it. Mathematics gets the kernel because it can; measurements get instruments because a kernel cannot run a stopwatch; designs get opposition because no formal system judges taste; and the human judges only what nothing else can. The whole method is this one allocation principle, applied without exception.

The hardware referee — a preview of honest non-uniformity

One more disclosure belongs in this chapter, because it completes the referee’s portrait. Mathematics has a single, uniform referee: the kernel. Hardware does not — and the paper discloses the structure of its hardware checking exactly because it is not uniform.

The hardware side is checked by a chain of three independent checkers across four links (Chapter 5 walks each one). Link 1 — from specification to emitted design artifacts — is kernel-checked in Lean. Links 2 and 4 — that the Verilog the toolchain consumes corresponds to the emitted artifacts, and that the synthesized netlist corresponds to that Verilog — are SAT-based equivalence checks (run with Yosys, an open-source hardware synthesis tool), and, the paper says plainly, they can only be that: as of 2026-08-11, no general Verilog-to-Lean importer exists in any public artifact, so a kernel cannot referee those links today. Link 3 is the synthesis miter — an equivalence construction that checks synthesis preserved the design’s logic.

And then the detail that shows the method eating its own cooking: the chain’s three checkers were built by three different agents, disagreed twice during the campaign, and were reconciled at the byte level — with the disagreements recorded in the ledger. Independent checkers that never disagree are probably not independent. Two reconciled disagreements are evidence the redundancy was real.

One last framing before the exercises, because it sets up everything the fleet chapters will show you. The referee’s deepest effect in this campaign was not any single bounce at the gate; it was what permanent, guaranteed bouncing does to behavior upstream. An agent that knows hallucinated proofs cannot land stops investing in persuasive wrongness — there is no audience for it; the gate does not read prose. The winning strategy under an incorruptible referee is the honest one, not because the agents became virtuous but because dishonesty stopped paying. Chapter 9 will give this observation its name — the kernel’s epistemics leaking outward — and the error ledger will show it happening on the record. Hold it as a hypothesis for now: ground truth shapes culture.

Exercises

1. The waterline audit. List the trusted base of: (a) a Lean proof under the campaign’s rules; (b) the same proof if native_decide were allowed; (c) a “proof” consisting of a frontier model’s detailed natural-language argument, reviewed carefully by you. Order them by size of trust base. Check: (a) kernel + 3 standard axioms; (b) adds compiler + runtime; (c) adds an entire language model and your own attention on a bad day — (c) is not smaller than (a) plus you; it replaces the kernel with you.

2. Elicit yourself. Take a feature you actually want to build. Write the one-paragraph prose objective, then attack it on the paper’s five axes (inconsistencies, completeness, population, negative space, ranked suggestions) as if you were the adversarial reviewer. Check: if you found nothing under “negative space,” you have not tried — every real objective deliberately excludes something, and unstated exclusions are where specs go to die.

3. Classify the failures. Three artifacts arrive: (i) a proof the kernel rejects; (ii) a kernel-passing theorem depending on a fourth, custom axiom; (iii) a kernel-passing, audit-passing theorem whose statement quantifies over an empty set. For each: which layer catches it, and what happens if that layer is missing? Check: (i) the kernel, automatically; (ii) the axiom audit — without it, the record silently absorbs an assumption; (iii) only statement-level human review via certificates and adversarial tests — no machine layer can catch it, which is why T(P)’s controls must be able to fail.

4. Price the two ends. The method leaves two duties human: elicitation at the front, certificate-reading at the back. For a system you know well, estimate the ratio of effort your team currently spends on those two duties versus everything in between (implementation, debugging, review of code). Check: most teams invert the Salt allocation — heavy in the middle, thin at the ends. The paper’s registers show where the errors actually live (statements and scopes, not proofs), which suggests most teams’ attention is pointed at the part machines are best at absorbing.

Common misreadings, corrected before they set

“The kernel proves the theorems.” No — the agents produce proofs; the kernel checks them. Generation and verification are different acts by different parties, and the method’s entire architecture lives in that difference.

“No human review means no human oversight.” Backwards — removing proof review is what funds the oversight that matters: every hour not spent re-deriving lemmas is spent on statements, designs, and rulings, where the recorded errors actually occurred.

“SAT links make the whole chain untrustworthy.” The chain is exactly as trustworthy as its per-link disclosure says, link by link — which is more than can be said for any chain described in one adjective. The alternative to a named SAT link is not a kernel link; it is an unnamed SAT link.

Chapter 3: The Twelve Articles

Most methodologies are designed in a conference room and then inflicted on a project. The Salt method went the other way, and the paper is specific about the direction: each of the method’s rules was minted from a practical failure — hallucinated results, plausible-but-wrong designs, measurements quoted beyond their scope — and the ledger records the incident behind every law. The method was not designed in advance and then applied; it accumulated as case law under the referee. That is why, the paper says, its articles read like a record of things that actually went wrong.

Above the twelve articles sits a three-clause creed — the paper’s Figure 1 prints it as the method’s header line, and every article below is one of its clauses made operational: truth is machine-checked only · structured opposition checks what the kernel cannot · human attention is the scarcest resource. You met these as the three commitments in Chapter 1; the articles are their case law. Read any article and you can name its parent clause: R2 and R4 descend from machine-checked truth; A4 and A6 from structured opposition; A2, A3, and A5 from the scarcity of human attention. The creed is what survives if you forget every article; the articles are what you need when the creed meets a Tuesday.

There are twelve articles in two tiers, and the tier boundary carries meaning. The six required invariants (R1–R6) are tool-agnostic — they state what the method is, independent of which models, provers, or repos you use. The six advisory articles (A1–A6) are the reference configuration — what this particular case study actually ran and measured. Swap Lean for another kernel-based prover, swap the fleet layout, and R1–R6 must survive unchanged; A1–A6 are one working answer, published so you can copy or contest it.

A note on the source: the paper commits the full method to a single figure (its Figure 1) that it says is designed to stand alone — the creed as header, the two tiers side by side, one line of gloss per article. That design choice is itself methodical: a method you cannot state on one page is a method your executors cannot be audited against. The card deck above is that figure, made interrogable; what follows is each card, unpacked with the failure it answers.

The required tier — what the method is

R1 — Five artifacts, at every level. Implementation, specification, kernel-checked proof, adversarial tests, certificates — from project design down to component design. You met the bundle in Chapter 1; R1’s content is the phrase at every level. A project whose components are verified but whose architecture is vibes is verified nowhere that matters.

R2 — No claim is admitted without its checker. The kernel for mathematics; the named instrument for measurements; structured opposition for designs. This is the article that generalizes the kernel’s epistemics to things kernels cannot touch. A measurement without its instrument named is an anecdote. A design without a refuter pass is a hope. Notice the three-way match: every claim type is paired with a checker type, and an unpaired claim simply does not enter the record.

R3 — The append-only ledger. All design decisions — including the human’s — are recorded in an append-only ledger whose distinctive content is the errors and retractions, amended at their source and recorded as first-class results. Append-only is the load-bearing property: you may add a correction; you may never make a past mistake un-happen. Chapter 9 shows this article carrying its greatest weight — a retracted measurement preserved forever, strike-through and all.

R4 — Statements are immutable. No statement is ever weakened to admit a proof. Statement changes are design-tier acts — never taken by an executor. Feel the failure this prevents: an agent is grinding on a hard theorem, and the fastest path to a green checkmark is to quietly narrow the statement until the proof fits. The kernel would bless the narrowed theorem happily — remember, it has no opinion on whether statements are worth proving. R4 makes the narrowing itself illegal at the executor level: an agent may fail loudly, but it may not succeed at a different problem than it was given.

R5 — Irreversible acts are human. A small class of irreversible, outward-facing acts — submissions, purchases, sends — is reserved to human hands, and the system’s job is to reduce each to a prepared click and stop. Not “ask permission,” not “proceed unless vetoed” — prepare, present, stop. Chapter 8 counts these clicks: 7 taken, 5 prepared and deliberately not taken. The clicks not taken are the article working.

R6 — Conditionals are allowed — and dispositioned. A statement may name hypotheses it does not discharge, provided each is named in the statement itself and carries a declared disposition: either to be discharged (ledger-owed, with the expectation of a future kernel proof) or out of domain (a stated trust boundary with another discipline — the paper’s example: semiconductor physics). And the closing clause with teeth: a program’s final deliverable carries no undischarged in-domain hypotheses. R6 is how a formal program talks about what it has not yet proved without lying: debt is fine; hidden debt is not.

See R6 on a concrete statement, because the disposition machinery is easiest to grasp with the hypotheses in view. A conditional result in the corpus has this anatomy (the instance is ours; the anatomy is R6’s):

theorem gap_bound_conditional
    (h_EH : ElliottHalberstam)            -- named IN the statement
    (h_phys : CellDelayModel)             -- named IN the statement
    : BoundedGaps k := …

-- dispositions, declared:
--   h_EH    : to be discharged  (ledger-owed; a future kernel proof)
--   h_phys  : out of domain     (trust boundary: semiconductor physics)

Everything R6 demands is visible in the type. The hypotheses are not in a README, not in a footnote, not in the author’s head — they are parameters of the theorem, so the kernel forces every downstream use to carry them. Anyone applying this theorem writes the hypotheses into their own statement, mechanically, forever; the debt cannot be laundered away by restatement. The disposition tags then split the debt into two honest kinds: to be discharged is a promise the ledger tracks — a future proof is owed, and the program’s final deliverable may not ship while it is outstanding; out of domain is a declared boundary with another discipline — the kernel will never model transistor physics, and pretending otherwise would be the lie. The rule’s closing clause — no undischarged in-domain hypotheses in the final deliverable — is what separates this from the common academic dodge of “assuming standard conjectures” indefinitely: conditionals are scaffolding, and scaffolding comes down before the building opens.

The advisory tier — the configuration as run

A1 — One orchestrator. A single master orchestrator on the top model class performs the most complex design work, passes routine work to executors — and owns the referee’s own infrastructure: audit tooling is never owned by a seat it audits. That last clause is a separation-of-powers rule. The seat that builds the axiom auditor must not be a seat whose work the auditor audits; a fox designing the henhouse lock is a recorded failure class, not a hypothetical.

A2 — Executors are the workhorses. Building, verifying, proving, refuting — and every task is classified by difficulty and priced before it is attempted. Pricing before attempting is what makes budgets (A3) meaningful: you cannot exhaust a budget you never set.

A3 — Budgets, loudly exhausted. Attempts are budgeted small, and an agent that exhausts its budget stops and announces its failure rather than grinding on. This is anti-slop machinery: the failure mode it kills is the agent that burns a night of tokens semi-randomly mutating a proof. A loud failure is information — it routes the task up for redesign. A silent grind is entropy.

A4 — Explore, then refute. Every major design phase has an exploration part and an adversarial refutation part, iterated until dry, with acceptance criteria pre-registered before the artifact exists. “Iterated until dry” means the refuter attacks until it finds nothing new — not until a schedule says stop.

A5 — Scheduled human interaction. Human interaction is periodic and scheduled — this program held a daily council with recorded rulings. The point is the cadence: the human is not an interrupt handler pinged per decision; decisions queue for the council, and between sittings the fleet works within pre-authorized law. Chapter 8 counts 20 council sittings across the campaign.

A6 — Independent witness. Every landing is verified by a second agent that did not produce it. Even with a kernel underneath, the producing agent could misreport scope, misregister provenance, or misstate what landed. The witness re-checks with fresh eyes and no authorship stake. You saw the pattern’s strongest instance already: three hardware checkers by three agents, two disagreements, both reconciled and ledgered.

One incident, four articles — the laws working together

The articles are not twelve independent rules; they interlock, and the interlock is best seen on a single incident. Here is a composite scenario — ours, assembled from the failure classes the paper names (wrong scope on a measured claim; budgets; witnessing; the ledger) — traced through the machinery:

Hour 0. An executor is asked to prove a bound and, mid-task, asserts in its landing note that “the corpus now exceeds 400,000 strict lines” — a number it estimated from memory to contextualize its work.

Hour 0, seconds later. R2 trips first: a measured claim has appeared without its instrument. The witnessing seat (A6) — which did not produce the landing and has no stake in its framing — checks the note against the extractor’s last published run, finds no supporting extraction, and flags it. The flag enters the append-only ledger (R3) with the next catch number.

Hour 1. The error is amended at its source: the landing note is corrected by an appended amendment (never an overwrite), the extractor is re-run, and the true number — with its command — replaces the estimate. Downstream documents that quoted the note re-derive.

Day 2. The incident recurs with a different executor. Two flags of one class is a pattern; at the next council sitting (A5) the human rules, and the ruling becomes law: measurement precedes assertion, and the extractor command travels with the number. The rule you met in Chapter 4’s fleet laws was, in exactly this way, minted — the paper’s articles “read like a record of things that actually went wrong” because that is what they are.

The portability test — what would survive a different stack

The two-tier structure makes a concrete prediction: swap every tool and the required tier survives verbatim. Run the test yourself, article by article:

This is what the paper means by calling the required tier tool-agnostic: it is the fixed point of the method under configuration change. When you evaluate any future “we used the Salt method” claim — and there will be such claims — the test is whether R1–R6 held, not whether the fleet looked the same.

Where the articles came from — the accidental foundry

The paper is disarming about the origin of all this law: the choice of mathematical foundation was, in some sense, accidental. The author set out to study the twin prime conjecture, and the method condensed out of that campaign — because hard mathematics under a kernel is an unforgiving proving ground. Every convenient shortcut an agent might take gets caught: by the kernel if it is a wrong proof, by the seats’ cross-checks if it is a wrong scope, by the refuter if it is a wrong design. Each catch became a flag; recurring flags became law.

And then the sentence that makes the method portable: nothing in the method requires it — we are not suggesting that one must work on twin primes before designing a chip. Any domain that pairs fast generation with an incorruptible checker could have forged the same laws; this one happened to be ours. Fast generation plus incorruptible checking — that is the entire precondition. Compilers with differential testing, protocols with model checkers, kernels with SAT solvers: the foundry is available wherever that pair exists.

Adopting the articles tomorrow — a minimal profile

You do not run a proof kernel. Can you run the required tier anyway? Here is a minimal translation to an ordinary software team — the mapping is ours; the point (that R1–R6 are tool-agnostic) is the paper’s:

The degraded profile is weaker than the real thing in one honest, specific way: without a kernel, your R2 checkers are corruptible, so your record’s floor is softer. But the structure — claims paired with checkers, errors first-class, statements frozen against executor convenience — transfers intact, and it is the structure, the paper argues, that the referee’s culture-shaping power flows through. Chapter 9 returns to exactly this transfer question with the paper’s own evidence.

The articles, measured — where each shows up in the record

A methodology paper’s articles are cheap to state and expensive to obey. What distinguishes this one is that the obedience is counted — nearly every article has a number somewhere in the paper’s registers testifying that it ran. The mapping, assembled from across the paper:

This table is also your reading guide for the rest of the lesson: every remaining chapter is one or more articles showing up in the data. When Chapter 6 refuses to print an unmeasured ratio, that is R2. When Chapter 8 corrects the human floor downward under machine proof, that is R3’s errors-as-first-class plus R2’s instrument discipline. When Chapter 9’s survey demotes two firsts, that is A4’s adversarial refutation aimed at the paper’s own claims. Method sections usually describe intentions; this one has receipts.

A closing observation on the two tiers, worth carrying into the fleet chapter. The required tier is written entirely in terms of claims and records — artifacts, checkers, ledgers, statements, hypotheses. The advisory tier is written in terms of actors — orchestrators, executors, councils, witnesses. That split is why the method ports: claims and records are universal to any serious work; actor topology is whatever this decade’s models and budgets make sensible. When the fleet configuration looks quaint in five years — and it will — the constitution underneath it is the part the paper expects to survive.

Exercises

1. The R4 sting. An executor cannot prove “the filter removes all duplicates” and proposes proving “the filter removes all adjacent duplicates,” noting the input is usually sorted. Walk this through the articles: which forbids the executor’s move, which tier must the change go to, and what artifact must be updated if the change is approved? Check: R4 forbids executor-side weakening; the statement change is a design-tier act (the council, A5, rules on it); if approved, the specification S and its certificates change — and the ledger (R3) records the decision and its reason.

2. Draft your own article. Pick a failure you have actually seen an AI coding agent commit twice. Write it as an article in the paper’s style: a one-line law, plus the failure that minted it. Check: the test of a good article is that it is checkable — someone auditing a transcript can say definitively whether it was followed. “Be careful with edge cases” is not an article; “no PR merges without a failing-then-passing test” is.

3. Sort the tiers. For each of: (a) “use the top model class for design work,” (b) “errors are amended at their source,” (c) “hold a daily council” — required or advisory, and why? Check: (a) advisory (A1 — a configuration choice about model tiers); (b) required (R3 — the ledger’s integrity is what the method is); (c) advisory (A5 — the cadence is one working answer; scheduled-ness generalizes, “daily” does not).

4. The creed audit. Take the three-clause creed and audit one AI tool you use daily against it: where does its truth come from, what opposes its outputs, and whose attention does it spend? Check: most consumer AI tools invert all three clauses — truth is model-asserted, opposition is absent, and the design spends your attention freely to save the model’s tokens. Feeling that inversion is the fastest way to understand what the Salt configuration is actually for.

Chapter 4: The Fleet

Method in hand, meet the machine that ran it. The configuration for this case study is five long-running AI agent seats sharing a repository and an append-only message bus, all directed by one human. This chapter walks the seats, the laws they operate under, the artifacts that move across the bus — and then reads the fleet’s most important output, which is not a theorem. It is an error record.

Five seats, one bus

The seats are roles, not model instances — long-running stations of responsibility:

Single out the evidence seat for a moment, because its existence is the fleet’s most transferable design decision. Most agent systems treat bookkeeping as exhaust — logs that accumulate, dashboards nobody audits. Here, measurement is a seat: a full standing role whose products — extractors, registers, the token meter, the human-time rubric, the silence-window instrument — are artifacts with the same review standards as theorems. Every number you will meet in Chapters 6 through 8 is this seat’s output. And A1’s separation rule applies with special force to it: the audit tooling this seat builds is owned by the orchestrator, never by a seat it audits — because an instrument owned by the measured is not an instrument; it is a press office.

Between them: a shared repository and an append-only message bus. Append-only is the same design decision as the ledger’s (R3), applied to communication: no message is ever unsent, no instruction silently edited after the fact. When Chapter 8 needs to prove which keystrokes were machine-authored, it is this property — a communication record nobody could rewrite — that makes the proof possible. The bus is not plumbing. It is evidence.

The laws in motion

The paper lists what daily operation under the articles looks like, and each clause is a chapter-3 article wearing work clothes:

Every landing is independently witnessed by a second seat. A result enters the record only after an agent that did not produce it verifies the landing. That one sentence — A6’s invariant — is all the paper specifies about the witness’s job.

Unpack what that job would have to involve — and label this clearly: what follows is our reconstruction of a plausible witness pass, not a protocol the paper publishes. What could a witnessing seat usefully do? Not re-prove — the kernel already did the proving, and re-proving would double the fleet’s cost for nothing. The natural checks are the cheap, decisive ones: replay the kernel check on the landed artifact; re-run the axiom audit; read the register entry against the artifact — does the stated scope match what was actually proved? do the provenance fields (landing date, commit) match the git graph? Checks of that shape target precisely the error classes the kernel cannot see. And who witnesses is as designed as what: a second agent that did not produce it (A6) — no authorship stake, no attachment to the framing, no incentive to wave its own work through. The pattern is code review’s oldest wisdom, transplanted: the author is the worst-positioned agent in the fleet to notice what their landing overstates.

Designs receive adversarial refuter passes before execution consumes them. Before the fleet spends a night of tokens executing a plan, a refuter attacks the plan — iterated until dry, per A4. Execution is expensive and amplifies whatever it is given; refutation is cheap and runs first.

Notice, too, what the bus architecture replaces. A five-seat team of humans at this tempo would drown in coordination — standups, handoff meetings, “quick questions,” status decks. The fleet has none of it, and not because agents are antisocial: the artifacts make most coordination unnecessary. A kernel-checked claim needs no meeting to be believed; a witnessed landing needs no status update — the record is the status; a loudly exhausted budget routes itself to the coordinator without a retrospective. Coordination cost is mostly the cost of transmitting trust between parties who cannot verify each other’s work; make every claim carry its own verification and the meetings dissolve into the bus. The one meeting that survives is the one that must: the council (A5), where the irreducibly human rulings happen — scheduled, recorded, twenty sittings in five weeks.

Measurement precedes assertion — and the extractor command travels with the number. No seat may assert “the corpus is 320,000 lines” from memory or estimate. The number is produced by a named extractor, and the command that produced it ships alongside it, so any seat — or any reader of the paper — can re-run it. You will see this article stamped on every table in Chapters 5–8: sizes annotated with their extractors, a denominator “reproduced first,” counts pinned to a single extraction commit.

Errors are amended at their source rather than corrected downstream. If a number was wrong in a register, the register entry is amended (append-only: with a correction entry, not an overwrite), and everything derived from it re-derives. Correcting downstream copies leaves the source lying in wait to poison the next reader.

Every attempt carries a budget, and failures are recorded alongside results. A3 in motion: the executor that cannot land its task within budget stops, announces, and the failure enters the ledger with the same standing as a success. A ledger of successes only is marketing.

The life of a theorem on the bus — the full data flow

Concept plus realization: here is one theorem’s complete journey through the fleet, from English to record. The stations are all the paper’s; the stitching narrative is ours.

Count the checkpoints between an agent’s idea and the record: pre-registered requirements, priced budget, kernel, axiom audit, independent witness, append-only registration. Six gates — and notice that only one of them is the kernel. The method’s texture is defense in depth around a single incorruptible core: the kernel guarantees the mathematics; the other five gates guarantee that what surrounds the mathematics — scope, provenance, process — is equally governed. Now, the report card that layered defense produced.

The observable consequence: an error record

Now the fleet’s report card, and the paper’s framing is deliberate: the observable consequence is an error record. Not “despite our method, some errors” — the error record is the observable, the thing the method promises to produce and govern.

Over the mathematics campaign, the system’s adversarial layers — the kernel first, then the seats’ cross-checks — caught design errors on a catch ledger whose numbering runs to #256. The bookkeeping is stated with the precision the method demands: the number is a monotone counter over the mathematics campaign’s append-only flags ledger, maintained 2026-07-07 to 2026-07-20; one number, #79, was never assigned; and later catches are recorded un-numbered and excluded from the count. Even the error counter’s own gap is disclosed — the ledger admits its skipped serial the way a bank statement admits a voided check.

What kinds of things got caught? The paper names the classes: wrong scope on a measured claim; stale citations; misattributed mechanisms; statement-level type traps. Look at that list carefully. Not one entry is “wrong proof.”

Pause on the ledger’s tempo, because it is easy to read past. The numbered window ran fourteen days (2026-07-07 to 07-20) and its counter reached #256 with #79 never assigned — on the order of eighteen numbered entries a day, every one recorded, named, and answered while the campaign sprinted at 56 commits a day. Most engineering organizations would experience eighteen recorded process-failures a day as a crisis; here it is the system operating as designed — the adversarial layers doing precisely what they were built to do, at fleet speed. The method’s bet is that error volume is not the enemy; unrecorded error is. A fleet that catches eighteen errors a day and records all of them is trustworthy; a fleet that reports two errors a week is either idle or lying.

And note what the seats can never do, no matter their budget or confidence — the negative space of the fleet’s powers, drawn by the required tier: no seat may weaken a statement to admit a proof (R4); no seat may own the tooling that audits it (A1); no seat may take an irreversible outward-facing act (R5); no seat may admit a claim without its checker (R2), assert a measurement without its instrument, or edit history (R3). The fleet is powerful the way a well-governed institution is powerful — enormous capacity inside hard constitutional walls. The paper’s phrase for the seats’ condition is exact: they operate under written laws that exist because the kernel’s ground truth makes them enforceable. Law without ground truth degrades into vibes; the kernel is what gives every other rule something solid to anchor on.

And the record’s integrity is not an honor-system claim — it is itself machine-checkable: all 73 registered headline theorems carry stated landing dates matching their landing commits, and all 59 landing commits are ancestors of the main branch. (Seventy-three theorems on fifty-nine commits — some commits land more than one result.) Anyone with the public repository can re-verify both claims mechanically: dates against commits, commits against ancestry. Provenance here is not a spreadsheet maintained by the authors; it is a property of the git graph.

The 73-on-59 anatomy repays one more beat of attention, because each half of the integrity check kills a different forgery. Landing dates matching landing commits kills backdating: you cannot claim a July priority for an August proof, because the commit’s position in the graph is the date’s witness. All landing commits being ancestors of main kills orphan claims: a theorem “proved” on some abandoned side branch that never merged is not in the record, however real its commit hash looks. Together they make the register a projection of the git graph rather than a document about it — and a projection can be recomputed by anyone, which is the only kind of provenance that survives its authors’ retirement.

One more disclosure completes the picture, and it is a model of scope discipline: a hand-classified breakdown exists for the first 78 numbered catches (classified 2026-07-15); the later catches are unclassified — and no class-dominance claim is made. The paper knows which error class looked most common in the classified slice, and refuses to say, because the slice is not the population. Hold that restraint in mind when Chapter 8 shows you what happens to a number quoted beyond its instrument.

The catch classes, illustrated

The four named classes of catch deserve faces, because each is a failure mode you have watched an AI assistant commit this week. The class names are the paper’s; the illustrative instances are ours:

Now the reading the paper wants you to take from the composition: the ledger’s composition is data about AI-assisted research. Not one of the four classes is a reasoning failure in the model’s chain of thought; all four are failures of claims about the world — scope, currency, attribution, formalization. If you govern AI work, this is the empirically observed threat model: not wrong proofs (the kernel has those), but right facts wrapped in wrong sentences. Design your checks there.

The human in the loop — counted, not described

Where is the human in all this? Present — but in a shape most “human in the loop” systems would not recognize, and the campaign registers count it rather than describing it:

The paper draws the structural conclusion: authority was reserved, not continuously exercised. Between rulings the fleet worked autonomously at the execution layer, no proof passing through human review. And the ledger records the pattern’s signature image: agents that reduced a theorem to one click and stopped, by design, because the click carried the human’s word. The fleet’s job was to make authority cheap to exercise — and then wait for it.

Step back once from the machinery and look at what the fleet chapter has actually described, because the paper’s quietest claim hides in the architecture’s familiarity. Seats with separated powers; an append-only record; independent witnesses; scheduled rulings; reserved final authority — this is not exotic AI engineering. It is the standard institutional design humans use wherever error is expensive and actors are fallible: courts, journals, aviation, clinical trials. The paper’s configuration is those institutions, miniaturized to run at machine tempo around one person — with the kernel playing the role no human institution ever had: a ground truth that cannot be lobbied. The transferable insight is that agent fleets do not need new social science; they need the old social science, implemented at the speed the agents actually move.

Exercises

1. Grade your Chapter 0 prediction. You predicted the split of the ledger’s catches between “wrong proofs” and “everything else.” The answer: wrong proofs contributed zero — not because none were generated, but because the kernel bounces them before the record, so they are caught upstream, not ledgered as record corruption. Check: if you predicted a nonzero share of wrong proofs in the record, notice what assumption you made — that the checker was a reviewer rather than a gate. That assumption is the sixty-year default the paper inverts.

2. The witness’s job description. A mathematics executor lands a theorem: kernel-checked, axiom-audited. List three distinct errors the landing could still contain that the witnessing seat must catch. Check: from the paper’s own catch classes — wrong scope in the register entry (“unconditional” for a conditional result); a stale or misattributed citation; a statement-level type trap (the theorem quantifies over a subtly wrong domain). All invisible to the kernel; all fatal to the record.

3. Design the bus query. Using only append-only ledgers — the flags ledger, the message bus, the git graph — sketch how you would mechanically verify the claim “all 59 landing commits are ancestors of main.” Check: extract each registered theorem’s landing commit hash from the register, then run an ancestry query per hash against main’s history. No testimony involved — which is the point: the integrity claim compiles down to git operations anyone can run.

4. Count your own gates. Trace one AI-generated artifact through your current workflow — a PR, a report, a config change — and count the independent gates between the model’s output and your record of truth. Check: the Salt count was six (requirements, budget, kernel, audit, witness, registration). If your count is one (“a human skims it”), note which of the four catch classes — wrong scope, stale citation, misattributed mechanism, statement-level trap — that single gate reliably catches. The honest answer is: none of them reliably, which is the paper’s empirical point.

Common misreadings, corrected

“A catch counter at #256 means the fleet was sloppy.” The catches are the adversarial layers working — at a tempo of thousands of claims. The sloppiness measure is record corruption, and that number is zero.

“The human barely did anything — 20 meetings and 7 clicks.” The counts measure command authority, not effort; Chapter 8’s floor shows 37+ engaged hours in under five days of the metered window alone. The finding is the shape of the effort — statements and rulings, never proofs — not its absence.

“Witnessing doubles the cost of everything.” Verifying a landing is not reproducing it: the expensive step was the search that produced the artifact, and nothing in A6 asks the witness to repeat it. On our reading, governance here is priced like inspection, not like reconstruction — and a witness rule did survive a 56-commit-a-day campaign, which bounds its cost in practice.

Chapter 5: The Spine

Here is the paper’s central artifact: a systems stack running from a theorem statement to a submitted physical design, with the verification of every link stated exactly. The paper calls it a chain of custody — the legal metaphor is earned, because the entire point is that at no step does the artifact pass through unexamined hands. And the construction speed is its own headline: the stack was built in seven days of elapsed repository history, inside the program’s five weeks.

The stack, top to bottom

Pause on the top of the stack, because it is the part most hardware papers do not have. This is not “we verified a CPU.” The chain starts at an application — with behavioral theorems about what the running program does — and descends through a compiler proved to preserve meaning, an executive proved to isolate, down to gates. A verified processor running unverified software proves little about behavior; custody has to start where the intent lives.

What each layer’s theorems actually say

“Verified X” is a phrase that means nothing until you ask: verified to do what? The paper names the theorem class at each layer, and the classes are the classical ones of the verified-systems literature — walk them slowly, because they compose:

The application’s behavioral theorems say: the program, as written in the structured source language, has the stated input/output behavior. Alongside them, the per-round kernel fixtures pin the claim to concrete rounds of the execution trace — the paper names the runW trace — so the abstract behavioral statement is anchored by kernel-proved instances a reader can inspect one round at a time. This is Chapter 1’s promotion machinery deployed at the top of the stack: the fixtures are tests that became theorems.

The compiler’s simulation proofs say: for each control construct — loops included, which is the hard case, since a loop’s compiled form must be related to its source across arbitrarily many iterations — the compiled code simulates the source semantics: every step the compiled program takes corresponds to a step the source program could take. Simulation is the standard currency of compiler verification (it is CompCert’s currency too), and its force here is transitive: a behavioral theorem proved about the source now transfers to the emitted instruction stream. You do not re-verify the application at the ISA level; the simulation proof carries it down.

The executive’s isolation theorems say: the multitasking layer preserves separation — one task’s misbehavior cannot corrupt another’s state. Isolation is the property that makes a stack compositional: with it, adding a task does not re-open every other task’s verification. Without it, “verified application” would be conditional on every neighbor behaving.

The switch’s routing theorem — the 1990 result — says: the rotation-based routing schedule composes to the identity, rot^k = id, the full rotation-closure result. The paper states exactly this much: the routing schedule the theorem certifies is proved in the kernel and drives the submitted switch. (Reading rotation-closure as the fabric’s self-routing guarantee — every stream returned to its intended lane — is our gloss on what such a schedule is for; the paper does not spell out the operational meaning.)

The four links — and the grade of each

Between the Lean world and the die sit four links. Chapter 2 previewed them; now walk them with the artifacts in hand. The chain’s stations: the specification and its kernel-checked development; the emitted design artifacts (hardware descriptions produced by a Lean-verified emitter); the Verilog the toolchain consumes; the synthesized netlist (the gate-level circuit synthesis produces); and the placed-and-routed die geometry.

Why can links 2 and 4 only be SAT? Because crossing from Verilog back into Lean requires an importer that gives Verilog a formal semantics inside the prover — and, as of 2026-08-11, no general Verilog-to-Lean importer exists in any public artifact. The campaign built its own importer, but the paper scopes it honestly: it handles this flow’s netlist-level Verilog, not general Verilog. So a kernel cannot referee those links today — a statement about the state of the world’s tooling, dated, checkable, and (knowing this field) temporary.

And name what even a perfect chain cannot see, because R6 has the vocabulary ready. Every checker in the chain — kernel, SAT, miter — judges logical objects: statements, netlists, Boolean functions. None of them models transistors, voltages, or clock skew; whether the fabricated silicon physically realizes the checked netlist is a claim belonging to another discipline entirely. The method does not pretend otherwise — it files that dependence exactly where R6 files such things: an out of domain hypothesis, a stated trust boundary with semiconductor physics (the paper’s own example for the category), held by the foundry and the cell libraries rather than by any proof. A verified stack is verified down to its stated boundary, never below it — and stating the boundary is what separates this chain from a marketing chain.

What does SAT-checked mean here? An equivalence check encodes two circuits into one Boolean satisfiability question — does any input make their outputs differ? — and a SAT solver searches exhaustively; unsatisfiable means no such input exists: the circuits agree on every input. A miter is the standard construction that wires the two circuits to shared inputs and XORs their outputs so that question becomes a single satisfiability instance. It is a genuine proof of input-output equivalence — but the paper refuses to blur it into kernel grade, because the trust base differs: you trust the solver, the encoding, and the tool that built the miter. Hence the design you already know from Chapter 2: the chain’s three checkers were built by three different agents, disagreed twice during the campaign, and were reconciled at the byte level — disagreements in the ledger.

The miter, drawn in text

Since two of the four links stand on it, see the miter concretely. You have circuit A (the emitted design) and circuit B (the Verilog the toolchain will consume). Build a third circuit:

        shared inputs x
        ↓            ↓
   [ circuit A ]  [ circuit B ]
        ↓            ↓
       out_A        out_B
          ↘        ↗
         [ XOR gates ]        -- bit-for-bit difference
              ↓
            diff              -- 1 iff A and B disagree on x

SAT question: does any x make diff = 1?
UNSAT  ⇒  no such x exists  ⇒  A ≡ B on every input

The solver’s answer is exhaustive, not statistical: unsatisfiable is a proof over the whole input space, produced by systematic search. So why is this a different grade from a kernel proof? Count the trust base, Chapter 2 style: you trust the SAT solver’s claim of unsatisfiability, the encoding of both circuits into clauses, and the tool that constructed the miter. Each is mature engineering; none is a proof kernel deliberately kept small enough to be the single, scrutinized point of trust. Same theorem-shape, bigger waterline — and the paper’s response is not to pretend otherwise but to triple the checkers and ledger their disagreements.

And what did the redundancy buy? Twice during the campaign, two of the three independently built checkers disagreed about equivalence. Sit with how alarming and how valuable that is: had there been one checker, one of those two moments would have been a silent wrong answer inside the trust chain. With three, a disagreement is a loud contradiction that must be reconciled — and both were, at the byte level, with the incidents in the ledger. Structured opposition (commitment two) is not a slogan; it is the difference between those two outcomes.

The sizes — measured, with extractors named

Every size in the paper’s component table carries its measurement basis — R2 stamped on a table. The components:

Add the Lean rows yourself — this arithmetic is ours, on the paper’s numbers: 5,067 + 11,001 = 16,068; + 4,251 = 20,319; + 1,884 = 22,203 Lean lines on the systems side. Notice the striking near-parity: 22,203 lines of Lean against 22,679 lines of agent-written Verilog — the verification development is the same order of size as the design it verifies, written in the same seven forge days, by agents.

Read the size table like an engineer for a moment, because the proportions carry information. The compiler’s 5,067 lines across 13 files is compact — a small structured language onto a small ISA, which is exactly the scoping a five-week program should choose. The executive-plus-application stack at 11,001 lines is the largest verified component — unsurprising, since it carries both the multitasking machinery and the behavioral theorems riding on it. The silicon flow’s 4,251 lines — importer, equivalence, cell models — is the Lean side of the SAT boundary: the machinery that lets link 1 emit and links 2–4 be checked. And the 1,884 lines of systems-side certificates are R1’s receipt: the reading surface was built as a first-class component, roughly a tenth of the verified code — the cost of keeping statements reviewable, paid in full and itemized.

One more design decision hides in the table’s first row, and it is the spine’s cleverest: the hardware is emitted, not translated. The kernel-checked development does not verify hand-written Verilog after the fact — a Lean-verified emitter generates the design artifacts from the checked development, so link 1’s guarantee is about the generator, once, rather than about each generated artifact separately. This is why Chapter 6’s provenance category is “kernel-emitted”: correctness flows forward through a verified producer. The alternative direction — importing existing Verilog into Lean to verify it — is exactly the missing general tool the paper documents; emission side-steps the gap for everything the emitter covers, and the SAT links exist to bridge the remainder.

Worked example — reproducing the RTL denominator

The RTL row carries a parenthetical that is a miniature lesson in measurement honesty, so let us reproduce it by hand. The silicon repository’s measured split, at a named commit, reports the full Verilog population as 316,911 lines across 119 files — a denominator the paper notes was reproduced first, before the split was quoted. Of that, flow-generated netlists — machine-produced gate-level output of the synthesis flow — account for 294,232 lines in 48 files and are excluded from the “agent-written” count.

Both checks close exactly, and the excluded share is worth staring at: 92.8% of the Verilog in the repository was written by no one — it is tool output. Quote “316,911 lines of Verilog” without the split and you inflate the authored work fourteen-fold. The paper’s habit — reproduce the denominator first, then publish the split with its extractor — is catch class “wrong scope on a measured claim” being prevented in real time. Chapter 6 runs entirely on this habit.

The fixtures, concretely — watching the application prove itself round by round

Close the chapter’s loop back to Chapter 1’s promotion machinery, because the spine’s top layer is its best illustration. The application’s execution is a trace — the paper names the runW trace — a sequence of rounds, each round a step of the running program with its inputs and outputs. An ordinary test suite would assert facts about a handful of rounds and run them in CI. The spine’s per-round kernel fixtures assert those same concrete facts — round three consumed this input and produced that output — but as theorems, proved in the kernel against the verified development. (The shape, in miniature: theorem round3 : runW w 3 = expected — a test’s content in a theorem’s clothing; the instance is ours, the mechanism the paper’s.)

Why bother, when the behavioral theorems already cover all rounds abstractly? Because the fixtures are certificates — the bottom rung of Chapter 1’s ladder. A reviewer who cannot absorb a quantified behavioral specification can absorb “round three: these bytes in, those bytes out, kernel-checked” — and the implication chain from the full spec guarantees the concrete claim understates rather than misleads. The fixtures are also the chain’s earliest tripwire: if an emitter change ever broke the application’s actual behavior, the concrete rounds break first and loudest, at the exact round that changed. Tests promoted to theorems keep every virtue of tests — concreteness, locality, readability — and shed their one vice, which is that nothing ever guaranteed the test suite meant what the spec meant.

What the spine is for

A word on the destination, because “taped out on a community shuttle” is doing specific work in the economics claim. Tiny Tapeout is a community silicon program: many small designs from many contributors are aggregated onto one shared die and fabricated together on a scheduled shuttle run, which is what makes real fabrication accessible at consumer prices — each design gets a small tile (this one’s is the 6×2 tile whose outline frames the paper’s die renderings). That choice is not a compromise the paper hides; it is the thesis completing itself. The claim was never “one person can run a foundry”; it was that consumer products end to end — consumer AI subscriptions for the fleet, a community shuttle for the silicon — now suffice to carry a verified chain from theorem to physical fabrication. The shuttle’s public record is also where the design’s files live (run 32284710003, commit 7d2b275), which means even the submission itself satisfies the method’s publish-and-replay standard: the artifact of record is on infrastructure the authors do not control.

The paper de-escalates its own hardware: we report the spine not as a hardware contribution — the design is modest. A small processor and a switching fabric on a multi-project community shuttle (Tiny Tapeout aggregates many small designs onto one shared die) would not impress a silicon conference, and the paper does not pretend otherwise. The claim is the chain: that one configuration can carry a single chain of custody from a theorem statement, through a verified compiler, to a taped-out physical design, with the trust boundaries named at each link. And riding the whole spine, the forty-year arc: the 1990 switching-network theorem, proved in the kernel in 2026 (rot^k = id — the full rotation-closure result), its certified routing schedule driving the submitted switch.

And read the seven-day number one last time with everything the chapter has assembled, because its meaning changed while you were not looking. On day one of this lesson, “a verified stack in seven days” sounded like a speed claim — impressive, suspicious. It is actually a reuse claim: seven days is what the spine cost given thirty days of forge — the method’s laws already minted, the fleet already disciplined, the referee already trusted — and given sixty years of verification research — Floyd and Hoare’s program logics forward — to stand on. The economics headline is not that verification became magically fast; it is that the method, once forged, amortizes: the second verified artifact costs a fraction of the first, and the paper’s five-week total prices the whole forge, spine included, at one researcher’s evenings. That amortization curve — not any single week — is what should interest anyone planning to be the second user.

Exercises

1. Attack the chain. For each link, name one error the link’s checker would catch and one it structurally could not. Check: e.g. link 1 catches an emitter bug that violates the spec, but cannot see anything about the Verilog text downstream; link 4’s SAT check catches a synthesis netlist that computes differently, but cannot check that the specification was right — no link checks intent; that is the front end of Chapter 2, forever.

2. Redo the split. A repository holds 402,000 lines of Verilog in 150 files; generated netlists account for 371,500 lines in 90 files. Compute the authored share, and state the one sentence that must travel with your number. Check: 402,000 − 371,500 = 30,500 authored lines in 60 files; excluded fraction 371,500/402,000 = 92.4%. The sentence: which extractor, at which commit, produced the denominator — reproduced before the split was quoted.

3. The importer question. Suppose next year someone publishes a general, trusted Verilog-to-Lean importer. Which links change grade, and what remains SAT or construction-based? Check: links 2 and 4 could become kernel-checked (import both sides, prove equivalence in Lean). Link 3’s obligation could move into the kernel too, given imported netlists — but synthesis itself stays untrusted; you would still be checking its output, not its code. The boundary moves; the method of naming it survives.

4. Name the grade. For each claim, name its verification grade in this stack’s vocabulary (kernel / SAT / miter / unchecked): (a) “the compiled loop behaves as its source”; (b) “the netlist matches the Verilog”; (c) “the Verilog matches the emitted artifacts”; (d) “the specification captures what the author wanted.” Check: (a) kernel — the compiler’s simulation proofs; (b) SAT, link 4; (c) SAT, link 2; (d) unchecked by any machine, forever — that is the front end, served by elicitation and nothing else. If you got (d), you have the paper’s deepest structure.

Common misreadings, corrected

“The chip is verified.” The paper never says this in one adjective, and neither should you. The honest sentence has four clauses — one per link, each with its checker named — and the discipline of saying all four is the contribution.

“SAT checking is the weak link, so the chain is only as good as Yosys.” Half right, importantly wrong: the SAT links’ trust base is bigger than the kernel’s, but it was checked by three independently built checkers that disagreed twice and were reconciled — redundancy engineered precisely because the base is bigger. Weakness acknowledged and instrumented is a different object from weakness ignored.

“Seven days for a verified stack means the proofs must be shallow.” The proofs are exactly as deep as their statements — simulation for the compiler, isolation for the executive, rotation-closure for the switch — and the statements are published, certificated, and interrogable. Speed changed who writes proofs, not what the kernel accepts.

Chapter 6: Provenance at the Die

“No RTL was written by a human” is easy to say. This chapter is about the harder discipline: saying exactly which parts of the physical design came from where — counted, at the die, by an instrument, with its scope sentence attached. It contains the paper’s single best worked example of measurement honesty, and we will do every division by hand.

Three kinds of authorship on one die

First, vocabulary — because the paper is surgical about a distinction most reporting would flatten. Logic on this die has three provenances:

The instrument that assigns provenance is the structural join: a per-cell census that matches named elements in the final geometry back to their source artifacts. The unit it counts is the flip-flop — the basic one-bit storage cell of digital logic. Flip-flops are the right census unit because they are the design’s sequential state: its memory, the part that carries information across clock cycles. Combinational logic computes; flip-flops remember; counting who authored the memory is counting who authored the machine’s state.

From RTL to GDS — the pipeline the numbers live in

The census’s two scopes correspond to two stations of the silicon pipeline, so build the pipeline first — this background is ours; every number attached to it below is the paper’s:

Now every number in this chapter has an address, and the scope discipline stops looking pedantic and starts looking necessary: the pipeline transforms the design at every stage — deleting logic at synthesis, inserting cells at placement — so a count without its stage name is not approximately right; it is unanchored. The same design honestly yields 966, 902, 1,468, 7,779, 14,636, and 43,884 as answers to “how big?” — six numbers, six stations, all true, none interchangeable.

The cast: MAC islands, serializers, and the fabric

Meet the blocks the census counts, because they recur in every number below. A MAC island is a multiply-accumulate unit — the workhorse arithmetic block that computes a running sum of products — laid out as its own island of cells; the design instantiates four, each kernel-emitted. A serializer converts a wide parallel word into a sequential bit stream for transport; the design pairs three of them with the active islands — and at the geometry the pairing is physical: each active MAC island is interleaved with its serializer, their cells intermixed on the die. Around them sits the switch-fabric core — the Batcher–banyan network of Chapter 5 — plus the clock tree and drive-strengthening the flow inserts. Kernel-emitted arithmetic, agent-written fabric and glue, tool-inserted clocking: all three provenances, physically interleaved on one small die — which is exactly why an honest census must go cell by cell.

The worked example — the flip-flop census, by hand

The provenance census is stated for the 2026-08-10 submission — the design the structural join has measured. Two scopes, both published:

At the die (post-synthesis, measured at the GDS — the final geometry file): the design carried 902 flip-flops of sequential state, of which 288 were emitted from kernel-checked Lean artifacts, and 614 came from agent-written RTL. Do the arithmetic in both directions:

At the RTL (pre-synthesis, counting what the source instantiated): the emission count was 352 of 966.

Now the beautiful part. Why do the two scopes disagree — 36.4% at RTL but 31.9% at the die? Subtract:

The same 64 flip-flops explain both gaps — and the paper tells you exactly who they are: a fourth kernel-emitted MAC island (64 flip-flops in RTL) was deliberately instantiated disabled and correctly removed by synthesis. (A MAC — multiply-accumulate — island is an arithmetic block; this one was wired disabled on purpose.) Synthesis saw logic that could never switch and optimized it away, exactly as it should. Because the removed island was entirely kernel-emitted, the die-scope percentage drops even though not one agent-written flip-flop changed. The census confirms the join is airtight at the geometry: it reaches all 288 named flip-flops with zero misattributions, measured at the GDS.

And the utilization number closes the physical picture: 56.27% design-instance utilization means the placed logic occupies a little over half the tile’s available instance capacity — a comfortably feasible design, not a heroic squeeze, which is consistent with the paper’s own de-escalation of the hardware as modest. The census’s value never depended on the design being large; it depends on the counting being exact, and exactness is easier to demonstrate on a die where every one of 902 flip-flops can be individually named, joined, and audited. A modest design with census-grade provenance beats an impressive one with estimated provenance — for this paper’s purpose, the modesty is almost a feature.

A second pass at the arithmetic — percentage points, decomposed

One more turn of the crank, because the two scopes teach a lesson about percentages that catches professionals weekly. The drop from RTL scope to die scope is 36.4 − 31.9 = 4.5 percentage points. Where exactly do 4.5 points come from, when only 64 flip-flops moved? Decompose it — this arithmetic is ours, on the paper’s numbers:

The removed island pulls the ratio in both directions at once — shrinking the kernel-emitted count drags it down, shrinking the total pushes it up — and the net effect depends entirely on the removed cells’ own composition (here: 100% kernel-emitted, so the drop dominates). This is why “the percentage changed” is never a finding by itself; the finding is the join — which cells, with what provenance, moved. An aggregate ratio is a shadow of a census; the census is the fact.

The shipped revision — and the number the paper refuses to print

Here the chapter turns from arithmetic to ethics, and it is the paper’s finest hour.

The design was revised before shuttle close; the shipped design of record is the revised submission. In the shipped revision, the kernel-emitted RTL re-derives exactly: four MAC islands and three serializers, 352 kernel-emitted flip-flops instantiated, the fourth island again tied disabled. The committed synthesis stat records 1,468 sequential cells in total. Everything about the shipped design is consistent with the measured 2026-08-10 submission.

So the shipped die-level provenance ratio is… obviously about the same, right? The paper will not say it. The structural join has not yet been re-run on the shipped run’s GDS, so no die-level provenance ratio is stated for the shipped design. The RTL re-derives exactly; the toolchain is the same; every engineer alive would bet the ratio is unchanged — and the paper still refuses, because the instrument has not run on that artifact. A number you have not re-measured is a number you do not print. The same refusal appears in the die-rendering figure: the per-cell provenance coloring is shown for the measured submission only, with the caption stating no percentages for the shipped run.

How the structural join works — and what “zero misattributions” certifies

The census instrument deserves its own paragraph, because its hardest problem is invisible until you have met a synthesis tool. Between RTL and GDS, the toolchain does not politely preserve names: logic is restructured, cells are cloned and merged, hierarchies are flattened. A naive “grep the netlist for the emitter’s module names” would miss and mislabel freely. The structural join is the instrument that survives this: it matches the named sequential elements in the final geometry back to their source artifacts structurally — and the paper reports its performance on the measured submission exactly: it reaches all 288 named flip-flops with zero misattributions, at the GDS.

Parse both halves of that guarantee, because together they are what “census-grade” means. Reaches all 288: completeness — no kernel-emitted flip-flop was lost to renaming; the join accounts for every one the emitter produced. Zero misattributions: soundness — nothing agent-written was mistakenly credited to the kernel-emitted column. A provenance claim with either property missing is an estimate wearing a census’s clothes; with both, the 288/902 is not a sampling statement or a confidence interval — it is an exhaustive count. And now you can hear the full weight of the chapter’s central refusal: an instrument this good, already built, already validated on the previous revision — and the paper still will not quote its result on a GDS it has not been run against.

Reading the geometry — what the die actually holds

The shipped design’s measured sizes, each with its basis, complete the picture — and hide one more scope lesson:

The paper renders the placed logic twice — two colorings of the same geometry — and the pairing teaches the chapter’s lesson visually. The function coloring answers “what does each region do?”: three MAC islands, each interleaved with its serializer; the formerly anonymous majority resolving into the switch-fabric core, the clock tree, and drive-strengthening. The provenance coloring answers “where did each cell come from?”: kernel-emitted versus agent-written versus tool-inserted. Same die, two orthogonal truths — and the figure’s method note explains why boxes would lie: because island and serializer cells are physically intermixed, per-function bounding boxes would overlap, so per-cell coloring is the faithful form. Fill and decap — the electrically passive padding and decoupling capacitance that occupy unused area — are not drawn, and the tile’s true die edge is outlined, so the logic is seen honestly against the space it actually occupies. Even a pretty picture, under this method, carries its measurement basis.

7,779 cells “at synthesis” versus 14,636 “placed” is not a contradiction — it is two instruments measuring two stages. Between synthesis and placement, the flow inserts cells wholesale: clock distribution from clock-tree synthesis, buffering, drive-strengthening. The paper’s rendering of the placed logic resolves what it calls the formerly anonymous majority into the switch-fabric core, the clock tree, and drive-strengthening — and notes the physical fact that each of the three active MAC islands is physically interleaved with its serializer, which is why per-function bounding boxes would overlap and honest coloring must be per-cell. Fill and decap cells are excluded from the drawing, and the 6×2 tile’s die area is outlined so the logic is seen against the true die edge. Even the picture has a scope sentence.

The category authored by nobody

Before leaving the die, spend a moment on the strangest of the three provenance categories, because it prefigures a debate the whole industry is about to have. Clock distribution inserted by clock-tree synthesis is, the paper says, authored by nobody — a category as distinct from agent-written as from kernel-emitted. No mind — human, model, or kernel — decided those cells individually; a deterministic tool computed them from constraints. Any census that forced them into “human” or “AI” buckets would be lying by taxonomy.

Now generalize, because your codebase has this category too: lockfiles, generated bindings, formatter output, build artifacts. The moment anyone asks “what fraction of this system did AI write?” — and auditors, regulators, and acquirers are all starting to ask — the honest answer requires exactly the Salt census apparatus: a defined unit, a named instrument, disclosed scopes, and a taxonomy with a nobody bucket. Chapter 5’s 92.8% flow-generated Verilog was this bucket at repository scale; the clock tree is the same bucket at die scale. The paper’s three-way split is not pedantry; it is the first fully worked example of a measurement genre the world is about to need constantly.

The chapter’s deepest export, before the exercises, is a reading habit you now own. Every provenance argument you will encounter from here on — how much of this codebase is AI-written, how much of that paper is generated, how much of the training set is synthetic — decomposes into the same four questions this chapter kept asking: what is the unit? what is the instrument? what is the scope? and has the instrument actually run on this artifact? The flip-flop census is the first published answer to all four at silicon grade, and its most instructive moment is the refusal — the number not printed because question four came back “not yet.” Carry the four questions; they are lighter than the numbers and worth more.

Exercises

1. Run the census backwards. Suppose the fifth revision enabled the fourth MAC island. Predict both scopes’ ratios, assuming nothing else changes and synthesis keeps the island. Check: RTL scope stays 352/966 = 36.4% (the source already instantiated it); die scope becomes 352/966 = 36.4% too — the scopes converge exactly when synthesis removes nothing. The divergence was the removed island; and note you just did what the paper would not — predicted an unmeasured GDS. The difference: yours is an exercise, labeled as such.

2. The headline audit. A journalist writes: “A third of Hickey’s chip was written by a theorem prover.” List every scope violation in that sentence. Check: (a) which third? — die scope 31.9% of flip-flops in the 2026-08-10 submission, not “the chip”; (b) “written by a theorem prover” conflates kernel-emitted (produced by a Lean-verified emitter) with proved; (c) the shipped design has no stated die ratio at all; (d) no mention that the count is sequential state, not all logic, and excludes tool-inserted cells. Four violations in eleven words — scope sentences exist because prose sheds them.

3. Choose the census unit. Why flip-flops and not Verilog lines, gates, or die area? Give one failure mode of each alternative. Check: lines — 92.8% of repo Verilog is flow-generated (Ch. 5), and formatting inflates freely; gates — combinational counts swing wildly under synthesis optimization; area — dominated by fill, decap, and drive strength, none of which is authorship. Sequential state is what survives optimization most meaningfully and defines the machine’s behavior — and even it, as the removed island shows, needs a scope sentence.

4. The six-number drill. From memory, place each number at its pipeline station and name what it counts: 966 · 902 · 1,468 · 7,779 · 14,636 · 43,884. Check: 966 = flip-flops instantiated at RTL (2026-08-10 submission); 902 = flip-flops at that submission’s GDS, per the structural join; 1,468 = sequential cells in the shipped revision’s committed synthesis stat; 7,779 = standard cells at synthesis (shipped — a synthesis count, not a placed census); 14,636 = placed standard cells (shipped, LibreLane); 43,884 = total instances (shipped, LibreLane). Six numbers, four instruments, two revisions — if you kept the scopes straight, you can read any hardware paper’s methods section now.

Common misreadings, corrected

“Only a third of the chip is verified.” Provenance is not verification grade: kernel-emitted counts what the Lean-verified emitter produced, while the agent-written remainder is still SAT-checked through the chain. The census answers “where did the state come from,” not “what is checked” — different questions, per the whole chapter.

“The disabled island was a bug synthesis fixed.” It was deliberately instantiated disabled and correctly removed — intent, execution, and measurement all agreeing. The interesting fact is not the removal; it is that the census caught its exact provenance signature (64 and 64) at the geometry.

“36.4% and 31.9% — the paper can’t decide.” Both, stated together, are the decision: scopes that answer different questions are published side by side, with the scope sentence traveling. One number would have been tidier and less true.

Chapter 7: The Forge

The mathematics campaign was not a demo attached to the chip project. It was the other way round: the mathematics was the forge of the method itself — the unforgiving proving ground where every article of Chapter 3 was minted from a failure. This chapter walks the forge’s output: the scale, the classical theorems it landed, and the strangest artifact of the whole paper — a machine-checked proof of the method’s own limit.

Thirty-seven days, zero silent

The shape of the campaign, from its published counts: 37 consecutive days (2026-07-06 to 2026-08-11), 2,087 commits in the mathematics repository, zero silent days — a mean of 56.4 commits per day (check it: 2,087 / 37 = 56.40… ✓), with a peak day of 178. The systems repository — the spine of Chapter 5 — received 1,379 commits over 7 days, with a peak of 343. Together: 2,087 + 1,379 = 3,466 commits — the number on this lesson’s hero. Both repositories began from empty trees atop the public mathlib library, first commit 2026-07-06; the system forge opened August 5, day 31 of the campaign.

Hold the asymmetry between the two repositories as you read the counts. The mathematics repository is a marathon: thirty-seven days, steady mean, every day active. The systems repository is a sprint: seven days at nearly triple the daily commit rate, racing a fixed shuttle deadline. Same method, same fleet, two entirely different tempos — which is itself evidence the discipline is load-bearing rather than ceremonial: rules that survive both a marathon and a deadline sprint are rules, not rituals.

Zero silent days deserves its emphasis before the milestones, because it is the campaign’s most human-legible statistic. Thirty-seven consecutive days — five weeks and two days — without one day of repository silence, through the mid-campaign family drive, through the shuttle deadline, through the survey morning. For a team, unbroken cadence is unremarkable; people rotate. For a configuration anchored on one person’s evenings and weekends, it measures the method’s core promise working: the fleet’s progress did not require the human’s continuous presence — only his rulings, delivered on the council’s schedule, with the silence-window instrument of Chapter 8 quantifying exactly how much landed between them.

Headline results arrived continuously, and the paper dates them by campaign day: unconditional bounded prime gaps on day 8; Chen’s theorem on day 10; the ¾-power zero-free region on day 13; the last headline theorem on day 29. Read that cadence against the field’s baseline: results of this class have historically been multi-year formalization projects for expert teams. Day 8. Day 10. Day 13.

The paper’s forge chart (its Figure 5) flags the milestones on the calendar itself, and the flags read like a syllabus of the campaign — from the opening sieve results through the classical pillars to the final systems landings. In the figure’s own labels, in calendar order: Brun bounded gaps (EH) · gaps ≤ 12 · SW + unconditional gaps · Chen · VMVT + ¾-power ZFR · HB master estimate · Jacobian verify · thm A2′ · log-Chowla terminal · T0 self-routing · payload + rot^k = id — with the system forge’s opening marked as the dividing line between the two stacked repositories. You do not need to recognize every label (several are the campaign’s internal names) to read the shape: conditional results first, unconditional strengthenings behind them, the deepest analytic machinery in the middle weeks — and then, in the final stretch, the flags stop being number theory and become hardware: T0 self-routing and the rotation-closure result are the 1990 theorem arriving on the die. One chart, both halves of the forty-year loop.

Worked example — calibrating the corpus against mathlib

How big is 37 days of fleet mathematics? The paper answers with the only calibration that means anything: against mathlib, the mathematical library the entire Lean community has built. And it publishes two counts under two named instruments — a raw line count, and a strict extractor that filters to substantive Lean (both counting methods publish):

Pause on what replayability means at this scale, because it is the corpus’s quietest superlative. A 658,103-line formal development is not a paper you skim; it is a codebase — and like a codebase, its health is a build status, not a reviewer’s impression. “Every theorem replays with one command” means the entire tower — pillars, wall, conditionals, certificates — re-checks from source on your machine, with per-theorem axiom audits confirming nothing snuck in. Compare the verification burden of the traditional alternative: the referee-years the mathematical community would need to human-review a corpus a third the size of mathlib do not exist, anywhere, at any price. Kernel-checked formalization is not just a way to validate work at fleet speed; for output at this volume it is the only way on offer — which is Chapter 0’s inversion, measured in reviewer-lifetimes.

Note the instrument discipline doing quiet work: the 29.3% compares raw to raw, measured with the identical extractor at the pinned revision. Comparing salt’s strict count to mathlib’s raw count would be flattering nonsense — a scope violation of exactly the class the catch ledger exists for. One fleet, 37 days, produced a corpus a bit under a third the size of the library a whole community built over years — measured apples to apples, extraction pinned to a single commit (2026-08-14, the extraction record published in the repository).

Calibrate that cadence against the field’s recent history, using only what the paper itself cites. The autonomous zeta-function result announced the day before this manuscript was drafted — a genuinely new bound, produced by Claude in roughly a day and a half of 31M output tokens — was validated by staff mathematicians, externally reviewed, and formalized: a single theorem, an event worthy of an announcement. The 91,000-line prime-gaps library was a landmark public release. Against that backdrop, read the forge’s tempo again: a Bombieri–Vinogradov–class pillar is not a lemma; any one of the nine would have been a formalization-community milestone announced on its own. Here they arrive on days 8, 10, and 13 of a five-week calendar, as waypoints — because the campaign’s goal was never any pillar; the pillars were the road. That is what changed economics looks like from inside: yesterday’s destination results become infrastructure you build on a Tuesday because the twin-prime road runs through them.

Two extractors, one honesty rule

Why publish two line counts — 658,103 raw and 320,000+ strict — instead of picking one? Because “lines of Lean” is a scope-sensitive quantity, and the paper refuses to let the reader guess which scope they are looking at. A raw count includes everything in the files; a strict extractor filters to what its published rules count as substantive Lean. Neither is the true count; they are two instruments, and both counting methods publish — so any skeptic can re-run either and any comparison can be made like-for-like. The mathlib calibration then does the only legitimate thing: raw against raw, same extractor, same pinned revision. Notice the ratio the paper does not print: strict-salt against raw-mathlib (which would read more impressively) — the flattering cross-scope comparison is exactly the catch class the ledger polices, and its absence here is the discipline holding under temptation.

Hold also the relationship between the two headline register counts, because readers conflate them: 73 registered headline theorems is the register’s count of major results with provenance trails (Chapter 4’s machine-checkable integrity claim); the nine pillars below are the subset of headline material that the priority survey supports as unproved-in-public before this corpus. Seventy-three is a bookkeeping fact about the register; nine is a surveyed claim about the world. Different grades — the Chapter 0 drawers again — and the paper never lets one borrow the other’s authority.

The classical pillars — stated at surveyed strength

Size is not substance, so here is the substance. The corpus carries machine-checked proofs of a set of theorems that are, to analytic number theorists, the classical pillars of the field’s twentieth century. The paper states their status at surveyed strength — a phrase Chapter 9 unpacks — meaning: as of 2026-08-11, per a five-lane adversarial survey, no public artifact in any proof assistant proves:

Why has none of this been formalized before, when the proofs have been in textbooks for decades? Because analytic number theory is formalization’s worst terrain (background ours; the priority facts the paper’s): the proofs run on estimates rather than identities — chains of inequalities with error terms that must be tracked to the constant, uniformly in several parameters at once; they lean on a deep bench of prerequisites (complex analysis, Dirichlet characters, zeta and L-function machinery) that must all exist in the library first; and the “routine” steps a paper dismisses in a phrase — partial summation, standard estimates — each explode into pages of formal bookkeeping. The community’s pace on this terrain has been years per pillar, which is precisely what made it a credible proving ground for a method claiming to change the economics.

The 2026 landscape the paper cites makes the same point from the outside. The verified prime-gaps library that went public mid-campaign (2026-08-08) is a serious artifact — 431 Lean files, 91,856 lines, sorry-free outside a deliberate comparator stub — and it carries the Maynard–Tao apparatus with bounded gaps ≤ 246… conditionally: Bombieri–Vinogradov is a named hypothesis in its own source. The frontier’s public state, in one sentence: the field’s best open artifacts still assume what this corpus proves.

For a sense of how far ahead of public formalization this list runs, the paper offers one devastating detail: a live external Bombieri–Vinogradov formalization project takes Siegel–Walfisz and the large sieve as named axioms in its own source — the community’s active project assumes as unproven inputs what this corpus proves, with proofs dated 2026-07 on a repository that was private until 2026-08-16, when it was made public.

The remaining pillars, in the same plain speech, so none stays a mere name (glosses ours; the list the paper’s): the Vinogradov mean value theorem controls the average behavior of exponential sums over many frequencies at once — the analytic engine that modern zero-free regions are built from; the Weil bound gives square-root cancellation for Kloosterman sums, arithmetic’s sharpest general estimate for a family of wildly oscillating sums, with algebraic geometry under the hood; the ¾-power zero-free region widens the strip where the zeta function provably has no zeros beyond the century-old classical shape — and wider zero-free regions convert directly into stronger prime-counting error terms; and the Matomäki–Radziwiłł / Halász machinery is the 2010s theory of multiplicative functions in short intervals — mathematics young enough that some of its authors are mid-career, formalized here within a decade of its creation. Nine pillars spanning a century of analytic technique, from de la Vallée Poussin’s era to 2016 — that range, more than any single item, is what “the classical toolchain, machine-checked” means.

To feel what landing these means, take the two the external project axiomatizes — the background gloss is ours; their status is the paper’s survey. Siegel–Walfisz is the statement that primes up to x distribute essentially evenly among the residue classes of a modulus q, with an error term controlled uniformly for q as large as any fixed power of log x — and that uniformity is the whole difficulty: the proof routes through the theory of exceptional zeros of Dirichlet L-functions, one of the most delicate corners of the subject. Bombieri–Vinogradov then says that although we cannot control any single large modulus, the error is small on average over moduli up to nearly √x — strong enough to substitute for the Riemann Hypothesis in a vast family of applications, which is why sieve theorists treat it as load-bearing infrastructure. Chen’s theorem and the bounded-gaps results of day 8 and day 10 stand on top of this machinery. Landing the pillars in order, at fleet speed, is what “the classical pillars on the way” means: the campaign built the twentieth century’s toolchain before attacking the twenty-first’s problem.

And the survey discipline cuts both ways — where near-simultaneous public artifacts exist, the paper downgrades itself: Vaughan’s identity, the Maynard–Tao sieve, and the Montgomery–Vaughan Hilbert inequality are reported as independent formalizations, not firsts, external artifacts cited, survey method and per-claim evidence published. Chapter 9 shows this machinery catching the paper’s own overclaims.

Private forge, public claim — how the dates hold together

A skeptic should immediately probe the timeline: the pillars are dated 2026-07 on a repository that was private until 2026-08-16. How can a private repo anchor a priority claim? Walk the mechanics, because they are sturdier than they first look. Git commits carry their history with them: when the repository went public, it went public with its July commit graph — the same graph whose integrity Chapter 4’s register check rides on (73 registered theorems, landing dates matching landing commits, all 59 landing commits ancestors of main). The priority claim itself is then scoped exactly as honest dating requires: the survey establishes that as of 2026-08-11 no public artifact proves the pillars — a statement about the public record on a stated date — while the corpus’s own proofs carry their July dates on a now-public, replayable graph. And the paper volunteers the residual softness rather than hoping you miss it: priority decays weekly (one competing library pushed commits during the final audit), the survey re-runs at submission, and “present and kernel-checked” is claimed while “authored” waits for the provenance split. Every date in the claim is doing stated, checkable work — which is precisely what most priority disputes lack.

Verifying the wall — the campaign’s strangest theorem

Before the wall, thirty seconds of background on the machinery that hits it — this history is standard and ours to summarize; the theorems about it below are the paper’s. The modern era of prime gaps began when Zhang (2013) proved that some bounded gap occurs infinitely often, and Maynard and Polymath (2013–14) rebuilt the sieve machinery so flexibly that the bound crashed from seventy million to 246, where it stands. The engine is a sieve weight: a nonnegative weighting of integers, engineered so that a weighted count of primes in k-tuples exceeds a threshold — and when a quantity M_k attached to the weight class exceeds 2, one concludes that two of the k tuple-slots are infinitely often simultaneously prime. Twin primes would follow from crossing that threshold at k = 2. Every improvement since 2014 has been a better weight; the open question was always how far the weight class itself could be pushed.

Now the ending the chapter promised. The program’s ambition was the twin prime conjecture — infinitely many primes p with p+2 also prime — and the paper states the outcome plainly: the conjecture remains exactly what it was. In the corpus it is a definition, never a theorem, and every conditional result names its hypotheses (R6, working as designed).

What the campaign produced instead is stranger and, the paper argues, more interesting: machine-checked theorems delimiting the method’s own reach. Some background, built from zero. The modern route to bounded prime gaps (Zhang, Maynard, Polymath) runs through sieve weights: assign cleverly chosen weights to integers, and if a certain quantity M_k associated with the weight class exceeds 2, you conclude that among suitable k-tuples, two elements are infinitely often prime simultaneously. Push M₂ above 2 with such a weight and twin primes would follow.

The corpus proves, in the kernel, that this cannot happen: M₂ ≤ 2 log 2 < 2 — no weight in the relevant Maynard class can cross the twin gate. Feel the arithmetic: 2 log 2 = 1.386…, comfortably short of 2, and the bound is proved sharp against the whole weight class — not “we couldn’t find one” but “none exists.” Alongside it: the least k with M_k > 2 is five — the machinery genuinely works, just not below k = 5 — and a formal gap theorem for parity-invariant sieve certificates, converting the folklore parity obstruction (sieves cannot distinguish numbers with an odd versus even number of prime factors) into kernel objects.

Unfold what proving the wall involved, because “the corpus proves M₂ ≤ 2 log 2” compresses a remarkable formal object. The statement quantifies over an entire class of sieve weights — every admissible weight of the relevant Maynard type — and bounds a variational quantity over all of them. Formalizing it means defining the weight class itself as a kernel object, defining M_k as an optimization over that class, and proving the bound holds for every member — including all the clever weights nobody has invented yet. That is a different species of theorem from “this particular sieve achieves X”: it closes a door on the future, not the past. The companion result — the least k with M_k > 2 is five — calibrates the door precisely: the machinery clears the bar at five simultaneous slots, and provably not below. And the parity-invariant gap theorem formalizes the deeper folklore: sieve certificates that cannot distinguish integers by the parity of their number of prime factors provably cannot close the remaining gap — the field’s oldest folklore obstruction, converted from lore into a kernel object with exact hypotheses.

A last word on what the forge means for mathematics itself, held carefully inside what the paper actually claims. The corpus adds no new headline theorem, and says so. What it adds is infrastructure: the pillars, formalized, public, and replayable, are now available to every future formal project the way mathlib’s algebra is — the external Bombieri–Vinogradov project’s named axioms, for instance, now have public discharge candidates. And the wall theorems add something mathematics has never had in this form: a machine-checked map of a barrier, against which any claimed twin-prime approach can be mechanically tested for whether it actually escapes the fenced class. Neither contribution is a headline; both are the kind of quiet capital that changes what the next decade of work costs. Infrastructure, as this paper keeps demonstrating, is the part that compounds.

Exercises

1. Pace arithmetic. From the published counts, compute: commits per day in each repo’s active window, and strict Lean lines per campaign day. Check: salt 2,087/37 = 56.4/day; saltworks 1,379/7 = 197/day (the system forge ran hotter); strict lines ≥ 320,000/37 ≈ 8,650/day. Then note which of these the paper itself refuses to convert to cost — all of them; Chapter 8 explains why.

2. The axiom mirror. The external BV project names Siegel–Walfisz and the large sieve as axioms; the salt corpus proves both. Under R6’s vocabulary, restate what each project has done, using “disposition” correctly. Check: the external project holds two in-domain hypotheses with disposition “to be discharged” (ledger-owed debts); salt discharged them. Neither is dishonest — naming your axioms is R6-compliant; the difference is who has paid the debt, and the survey’s job is establishing that no public artifact had.

3. Explain the wall to an engineer. In three sentences, no number theory: what does M₂ ≤ 2 log 2 < 2 tell a lab that wants to spend a billion agent-hours on twin primes via Maynard-class weights? Check: the entire strategy class is proved dead — not hard, dead; any budget spent optimizing weights in that class is spent finding what the kernel already knows cannot exist; progress requires machinery outside the class (and the parity theorem fences part of that too). Negative results are compute-savers — that is why verifying the wall is a research product.

4. The strength audit. Sort these chapter claims by evidentiary grade, strongest first: (a) M₂ ≤ 2 log 2; (b) “no public artifact proves Bombieri–Vinogradov”; (c) 29.3% of mathlib; (d) “hard mathematics under a kernel is an unforgiving proving ground.” Check: (a) kernel-grade — replayable by you; (c) instrument-grade — identical extractor, pinned revision, re-runnable; (b) surveyed-grade — adversarial, dated, demotable by tomorrow’s upload; (d) the paper’s interpretation — plausible, argued, and not a measurement. Four sentences from one chapter spanning four grades: if you sorted them cold, Chapter 0’s drawers are now furniture in your head.

Common misreadings, corrected

“The AI proved theorems humans couldn’t.” Every pillar is a known result with a published human proof; the campaign’s contribution is machine-checked formalizations at unprecedented speed and completeness — and the paper says “no new headline mathematics” in its own limitations before any critic could.

“They failed at twin primes.” The program aimed at twin primes and reported exactly what it earned: the pillars, and a kernel-checked proof that the standard route cannot reach the target. In mathematics, precisely locating a wall is not failing to find the door; it is cartography — and this map is machine-checked, which no prior sieve-barrier discussion could say.

“29.3% of mathlib in 37 days means quality must be low.” Line counts measure size, and the paper offers them only as size — calibrated, same extractor, both methods published. The quality claims ride elsewhere: on the kernel (every line checks), the axiom audits, and the survey’s per-claim evidence. Volume and rigor are separate columns here, which is exactly why both instruments publish.

Chapter 8: The Economics, Governed

Every AI-productivity paper you have read opens its economics section with its most impressive ratio. This one opens with a list of ratios it refuses to compute — because, it says, the temptation in this genre is to print ratios the records do not support. That refusal is the chapter’s thesis. The numbers that follow are remarkable; the governance of the numbers is the finding.

First: what cannot be derived

From this project’s records one cannot derive: a dollar cost per theorem — subscription pricing carries no per-request prices, so any dollar figure would be an invention; model-hours; a per-account attribution; or a generated-versus-authored split of the Lean corpus — until that split is published, the corpus supports “present and kernel-checked,” not “authored.” Four viral headlines, declined in one paragraph. The figures below are what the records do support — each under a named instrument.

Each refusal has a specific evidentiary reason, and the reasons teach more than the refusals:

Notice these are the four numbers every journalist, investor, and lab-strategy deck most wants. The paper’s position is not that they are unknowable in principle — a differently instrumented campaign could meter them — but that this record does not support them, and printing them anyway would be the exact catch class (“wrong scope on a measured claim”) the ledger spent five weeks catching. The economics section of an AI paper is where scope discipline goes to die; this one opens by refusing the temptation in writing.

The instruments, cataloged

What the chapter does publish comes from four named instruments — keep their scopes distinct, because every number below belongs to exactly one of them:

The metered window — a pre-registered instrument

The token numbers come from a meter pre-registered before its data accumulated — instrument and pre-registration published. Pre-registration matters for the same reason it matters in clinical trials: an instrument chosen after seeing the data can be chosen because of the data. The meter covers a 4.86-day window at campaign end. Its totals:

Now the worked arithmetic — ours, on the paper’s numbers, every division honest:

The paper’s own stated ratio is 376 output tokens per inserted line — and it arrives wearing its scope sentence: a figure whose numerator includes all prose and design work in the repository, resting on a broader insertion base than the Lean-only count (divide tokens by Lean lines alone, as we just did, and you get ≈493 — the ratio moves by a third depending on which denominator the record supports; the paper prints its figure with the caveat attached precisely so readers cannot silently re-derive a flattering variant). And a second caveat, stated as a headline rather than a footnote: the figure must not be extrapolated to the full corpus — the meter postdates every headline theorem. The window saw late-campaign consolidation work, not the days Chen’s theorem landed. The paper calls this the study’s largest measurement gap, not a footnote.

One hand-check on the window itself, before trusting anything computed from it — do the days-to-hours conversion:

Small checks like this are how you read instrumented papers: internal consistency between independently quoted figures is cheap to verify and catches transcription drift — the numbers here close. Now the window’s hardest measurement.

Human time — a floor, held to machine proof

How much human attention did 4.86 days of fleet work consume? A published-rubric extraction bounds the human’s engaged time at 37h21m across 45 blocks, out of the window’s 116h40m of wall clock. By hand:

But the number’s history is the real lesson. The first extraction said 44h25m. It was corrected downward to 37h21m after a cross-seat audit uncovered something unsettling: the transcript channel carries machine-authored keystrokes. A coordinating agent nudging fleet seats by terminal injection arrives with human provenance fields — indistinguishable, at the record layer, from a hand at the keyboard. Correlating the transcripts against the sending seat’s own logs (instrument published) proved 11h50m of such machine traffic inside the window — including, the paper notes, orders the author explicitly disowned on the record.

Check the deltas: 44h25m − 37h21m = 7h04m removed, yet 11h50m of machine traffic was proven. The gap is the rubric’s mechanics (our reading of it): engagement blocks bridge gaps up to twenty minutes, so a machine keystroke inside a block that genuine human touches also anchor removes nothing — only blocks that existed solely on machine traffic fall out. And a 4-minute band whose authorship the record cannot settle is excluded and reported, never folded in.

One more derived texture from the rubric — ours, from the published counts: 2,241 engaged minutes across 45 blocks averages 2,241 / 45 ≈ 50 minutes per block. The picture is not a person glancing at a dashboard; it is repeated, substantial working sessions — roughly nine per day of the window — woven through 117 hours of wall clock in which the fleet never stopped. Remember what those sessions contain, per the three commitments: statements, designs, and rulings. Not proof reading. Never proof reading.

Place the window on the campaign’s calendar to complete its scope picture — the placement arithmetic is ours. 4.86 days at the end of a 37-day campaign is about 13% of the calendar, and by the paper’s own dating it sits after day 29’s final headline theorem: the meter watched consolidation, systems work, and the push to submission — not the sprint that landed Chen. Both consequences follow honestly. You cannot scale the window’s totals by 37/4.86 to estimate the campaign — the paper forbids exactly that, because the workload differs in kind. But within its window the meter is complete: every output token, every deduplicated request, every commit and inserted line, under a pre-registration that predates the data. A small, airtight window beats a large, leaky estimate — that trade is the instrument’s entire design, and the paper names the residual (the unmetered majority of the campaign) as its largest measurement gap rather than quietly hoping the window reads as the whole.

Why do consumer subscriptions matter enough to appear in the abstract? Because they are the access claim. On metered enterprise APIs, this campaign’s token volume would be a corporate line item; on consumer subscriptions, the marginal cost of the fleet’s week is the subscription fee — which is what makes “who can afford it” (Chapter 0’s question) answerable with “one person, no grant.” The flat-rate structure is also, note the symmetry, exactly why no dollar-per-theorem exists: the same pricing that democratizes the work erases its per-unit cost records. The paper accepts both halves of that bargain and states them together.

Silence windows — measuring autonomy in both directions

The claim “the fleet ran autonomously” needs an instrument too, and the paper defines one. A silence window is the stretch between consecutive human touches to any personal-lane seat — every agent session on this program’s side of the author’s employment firewall. It is a claim about direction, not sleep — and coverage is disclosed: commits predating the earliest readable transcript are excluded rather than counted as silent. The instrument runs over the full campaign, not just the metered window, and bounds autonomy in both directions — how much landed without direction, and how thin the un-directed tail really is:

Turn the percentages into commits — the conversions are ours, on the paper’s totals — and the table becomes vivid. In the mathematics repository, 43.0% of 2,087 commits is roughly 900 commits that landed with no human having touched any seat for at least an hour; 8.8% is roughly 184 commits inside eight-hour-plus silences — work landing in the depths of genuinely unattended stretches. And the systems row hands us a satisfying cross-check: 0.1% of 1,379 commits is 1.4 — and the paper indeed reports a single commit at the eight-hour threshold. The percentage and the count agree. ✓ Instrumented papers earn trust in exactly these small collisions between independently stated figures.

The longest silence window containing landings ran 20h56m and carried 26 commits with 12,310 inserted Lean lines — nearly a full day of unattended mathematics. The systems repository was driven more interactively, exactly as you would expect for a week racing a shuttle deadline. Unattended night operation under standing evening orders was part of the configuration throughout — stated in silence-window form because the clock-hour version (18.1% of mathematics commits landed 21:00–05:00 local) is the thinner claim, reported once so no reader need compute it.

And the paper polices its own romance: we state what silence does not mean. The designs executing inside a silence window were frozen and refuter-attacked before the window opened; the claim is that the execution loop ran without direction — not that work appeared from nowhere.

Two clarifications keep the floor honest in the directions readers stretch it. Nights included means the 116h40m denominator is raw wall clock — no sleeping hours deducted — so the ≈32% engagement figure is computed against the harshest possible base; against waking hours it would read higher, and the paper declines that flattering renormalization. And the 45 blocks are the rubric’s segmentation, not the calendar’s: a block is a run of touches bridged across gaps of up to twenty minutes, so the count measures sustained engagement episodes — which is why dividing minutes by blocks (≈50 per block) describes sessions, not interruptions. Instrument-grade numbers survive exactly this kind of prodding; that is what the grade means.

Authority, itemized — reading the click ledger

Chapter 4 tabulated the governance counts; here is what they mean as economics. Twenty council sittings over a 37-day campaign is roughly one ruling session every two days — scheduled, not reactive. Seven irreversible acts — submissions, purchases, sends — against five prepared acts deliberately declined: a 7-to-5 ratio of clicks taken to clicks refused, which is the paper’s “authority reserved, not continuously exercised” rendered as data. A system optimized to please would have a decline rate near zero; a decline rate this high says the prepared-click pipeline presented real choices, not rubber stamps. Add the single design veto and the nine source verifications — checks only a human with the paper or the vendor portal could perform — and the human’s entire command-authority footprint over five weeks fits in a table you can read in ten seconds.

Set the two headline fractions side by side and the division of labor becomes almost diagrammatic: the human was engaged for ≈32% of the metered window’s wall clock — but proof review consumed 0% of it, and 43% of the mathematics repository’s commits landed in windows where no human had touched any seat for at least an hour. Engagement concentrated at statements, designs, and rulings; execution ran under law. That allocation — not any single ratio — is the economic finding.

The arc of the role

The chapter’s numbers get their meaning from a story the paper tells straight. In the campaign’s first days the author drove everything: each theorem began as a conversation, model configurations were swapped by hand for every design run, and he stayed attentive through the nights. Mid-campaign he drove eight hours each way, on a weekend, to visit family — laptop tethered to his phone, powered from an oversized battery, pulling off at highway ramps whenever a theorem finished — so that no decision would wait on his absence.

What changed over the five weeks, the paper insists, was not the amount of engagement — the transcripts show it grew — but its kind: the machinery he once operated by hand became law-governed and pre-authorized; decisions moved up the stack from mechanism to statement; the referee held the floor in between. By the final week the fleet ran its nights with landings in his silence, and the author reports the configuration’s most personal measurement himself: he sleeps untroubled. His curiosity has its own category in the pre-registered rubric — watching, redirecting nothing — counted as its own line, proudly.

Before the exercises, assemble the chapter’s parts into the single picture they were measuring. One person, roughly nine fifty-minute sessions a day, none of them reading proofs; a fleet consuming twenty-eight million tokens in under five days, its every request metered; forty-three percent of a mathematical repository’s commits landing in stretches where no one had touched it for an hour or more, under designs frozen and attacked before the silence began; and a rulebook that counted the human’s refusals as carefully as his acts. Whether this configuration is the future of research, the paper explicitly does not claim. What it claims — and instruments — is that the configuration existed, ran for five weeks, and left records precise enough that you have just spent a chapter re-deriving them by hand. Existence proofs with measurements attached are how new regimes announce themselves.

Exercises

1. The forbidden ratio. Using this chapter’s numbers, construct the most impressive-sounding ratio you can that the paper would refuse to print, and say exactly which rule it violates. Check: e.g. “a headline theorem every 100M tokens” — violates the extrapolation ban (the meter postdates every headline theorem) and invents a numerator the records don’t attribute. If your ratio involved dollars, you failed twice: subscription pricing carries no per-request prices.

2. Audit the floor’s direction. Suppose the correlation instrument had errors in both directions: it sometimes misses machine traffic, sometimes flags real human typing as machine. Which error inflates the paper’s thesis, and what does the stated policy do with each? Check: flagging real human typing as machine shrinks the floor — the self-serving direction — so such exclusions require machine proof; missed machine traffic leaves the floor too high, which is the direction the paper accepts, because a floor that errs high is still a floor. That asymmetry is the whole design.

3. Design a silence instrument for your own agents. Define, precisely enough to implement: a “touch,” a window, the coverage disclosure, and the one sentence about what your silence metric does not mean. Check: your definition must decide the hard cases the paper decided — scheduled cron nudges (machine, not touches), sessions outside the measured lane (excluded, disclosed), unreadable history (excluded rather than counted as silent). If your metric can be gamed by turning off logging, it counts absence of evidence as autonomy — the exact bug the coverage clause exists to kill.

4. Build the floor for your team. Adapt the self-serving-direction rule to a measurement your team actually publishes (test coverage, incident counts, model win-rates). Identify the self-serving direction, then specify what evidence standard that direction requires. Check: for coverage, deletions from the denominator are self-serving (excluding “untestable” files) — so exclusions need a machine-checkable rule, not a judgment call; for incidents, closing tickets as duplicates is the self-serving direction. If your policy assigns the higher burden to the flattering direction, you have imported the chapter’s one indispensable sentence.

Common misreadings, corrected

“37 hours of work produced all this.” The floor covers 4.86 days at campaign end — nothing about the other 32 days, when the transcripts show engagement grew over time. Scaling the floor across the campaign is the exact extrapolation the instrument forbids, in both directions.

“376 tokens per line of proof.” Three scope violations in six words: the numerator includes all prose and design work, the denominator is inserted lines (not proof lines), and the window postdates every headline theorem. The corrected sentence is longer and true — the trade this whole lesson keeps making.

“43% autonomy means the fleet mostly ran itself.” The silence instrument measures direction, not contribution — and the paper immediately bounds the romance: designs were frozen and refuter-attacked before windows opened, and no landing-bearing silence exceeded 21 hours. Autonomy here is a measured tail with a stated ceiling, not a vibe.

Chapter 9: Errors as Results & What It Means

Most papers bury their mistakes. This one promotes a mistake to a result — the paper’s own phrase: “And one retraction, reported as a result.” This closing chapter reads that retraction, the survey that demoted the paper’s own claims on its final morning, the limitations stated at full strength — and then steps back to what the whole case study means for anyone building agent systems.

The retraction — the thesis in miniature

Mid-campaign, the project measured a verification-cost ratio — the classic genre number: how much extra does verifying cost over just building? It published the ratio internally. The same day, a second run of the measurement arrived — of three runs in all — and the ratio swung by a factor of 52. One of the three runs fell inside the very 10–100× overhead range the published claim had denied.

Think about what a 52× swing means: the measurement was not slightly imprecise; it was not a measurement. Three runs of the same instrument produced answers spanning nearly two orders of magnitude — the instrument had no stable object to measure, or no stability in measuring it. Any single run, published alone, would have been an authoritative-looking accident.

The response is the method executing under fire. The claim was struck the same day. The retraction stands in the ledger — append-only, so it is a visible strike-through with commit hashes (5fa8987 → 8520580), not a deletion — with a standing instruction never to quote a ratio of that class again. Not “remeasure more carefully”: the incident was converted into law, exactly the case-law dynamic of Chapter 3. And the paper explains why it tells you at all: it is the paper’s thesis in miniature — the configuration’s value is not that it produces impressive numbers, but that its numbers are governed.

First, why a cost ratio is the natural place for this method’s one public stumble. Of everything the campaign measured, a verification-cost ratio is the quantity most exposed to instability: its numerator and denominator are both durations of complex, cache-dependent, configuration-sensitive toolchain runs, and a ratio of two noisy quantities amplifies the noise of both. It is also the genre’s most quotable number — the one every reader of a paper like this wants — which is precisely the combination the method treats as radioactive: maximum demand, minimum stability. The instrumentation did not prevent the error; nothing prevents first measurements from being wrong. What it did — and this is the result — is make the error short-lived and educational:

Lay the retraction out as a timeline, because its speed is the finding:

And mark the irony the paper surely intends: the number that had to be struck was the verification-cost ratio — the very statistic sixty years of literature used to argue verification does not pay, and the statistic this paper’s admirers would most love to quote in its favor. The method killed its own best marketing number for cause. If you want a one-line test for whether an organization means its epistemics, this is it: what happens to a flattering number that fails its re-run?

What the referee exports

The paper’s qualitative finding is a sentence you should sit with: the kernel’s epistemics leak outward.

A fleet of AI agents whose native failure mode is confident error spent the campaign catching each other’s scope claims, retracting at the source, and converting incidents into written laws — because an incorruptible ground truth existed to anchor the culture. The error ledger shows the classes the culture caught: measurements published with the scope of laws; registers asserting world-state instead of measuring it; instruments trusted across configuration boundaries they were never validated for. Each class was caught, named, and answered with a mechanism — by the agents, on the record. The agents did not become better predictors; they became better citizens of a record, because the record had a floor nobody could argue with.

Read the three exported error classes again slowly, because each is a pattern you can hunt in any agent system today (illustrations ours, classes the paper’s):

The final-morning survey — the system attacks its own claims

On the study’s final morning, the fleet ran a priority survey against its own results: five adversarial search lanes over the live literature, hunting for prior art that would demote the corpus’s believed firsts. It found some. Two of the corpus’s believed firsts had public predecessors — one under a different name that no text search could see. The claims of Chapter 7 are stated at exactly the strength that survey supports — that is what “at surveyed strength” has meant all along, with the survey method and per-claim evidence published, and a re-run scheduled before submission per the survey’s own cadence ruling.

The survey’s mechanics reward a closer look, because “we searched for prior art” is the least trustworthy sentence in academia and this one is built differently. Per the paper’s own reference to it, the instrument is a merged verdict over five adversarial search lanes evaluating twelve claims — lanes constructed to find predecessors, not to confirm their absence, with per-claim evidence files published and an “as of” date stamped on the verdict (2026-08-11). The adversarial construction is what gives a negative result standing: a search that wants to find nothing, finds nothing, always; a search built to attack — five different ways, merged — and that still comes back empty on nine claims while catching two real predecessors on others has demonstrated its teeth on the same run that produced the negatives. It is T(P)’s “every control must be able to fail” applied to literature search — and the two demotions are the controls failing honestly, in public, which is why the surviving nine claims are believable.

The limitations, at full strength

The paper’s limitations section reads like an adversary wrote it, which by A4 is roughly true. In full:

Add the discussion’s own boundary markers: the inversion is claimed only in a specific regime — when generation is fast, cheap, and fallible — and the records show the configuration’s edges: the SAT links, the autonomy tail (no silence window with landings exceeded 21 hours), the measurement gaps. The narrow demonstrated claim: machine verification is what turned a fleet of generative models into a research instrument whose output can be trusted at the campaign’s measured pace — 2,087 commits in 37 days, zero incorrect proofs reaching the record — with the complete accounting, errors included, now public.

Set the limitations’ length against the field’s norms for a moment. Seven confessed limits, one of which (“no new headline mathematics”) preemptively deflates the claim every headline about this paper will make anyway, and another of which (the economics gap) the paper elevates from footnote to named largest weakness. Papers do not usually compete to state their own softness this precisely; this one does because under-claiming is load-bearing for its thesis — a paper about governed numbers that inflated its own would be self-refuting in a way no referee would miss. The limitations section, in other words, is not damage control. It is the demonstration, still running.

What would change the paper’s mind — and yours

A thesis this confident should name its falsifiers, and this one’s are readable off its structure. The inversion claim would break if: the kernel-checked record were shown to contain an incorrect proof (the paper stakes everything on zero — one counterexample ends the story); the provenance registers failed their own mechanical checks (dates not matching commits, landing commits off main’s ancestry); the pre-registered instruments were shown registered after their data (the pre-registrations are published precisely so this can be checked); or replaying the corpus produced kernel failures. Every falsifier is public and mechanical — no access to the author required — which is the practical meaning of “the most completely documented instance” in the abstract: not that you should believe it more, but that disbelieving it correctly has been made cheap.

And when the next Salt-style claim crosses your feed — it will; the economics guarantee imitators — this paper hands you the audit questions: Where is the incorruptible checker, and what claim types does it actually cover? Where is the append-only error record, and does its volume look like a working system (eighteen a day) or a press release (two a week)? And which direction of error is self-serving — and does the higher burden of proof sit there? Three questions, answerable from artifacts, no trust required. That checklist may be the paper’s most durable contribution: it teaches the reader to referee.

Lineage, disclosure, and where this lands

The verified-stack lineage the paper claims — the CLI stack, CompCert, seL4, CakeML — consists of landmark artifacts by expert teams over years; the paper positions itself as changing their economics, not their depth. Its disclosure is equally direct: the agents are Claude-family models (Anthropic) operated under consumer subscriptions; the work is a month-long collaboration between the author and Claude; text and figures may carry content-provenance marks; no AI system is an author, and the author takes full responsibility — reserving to himself, as the contribution statement says, all statements of results, designs, and rulings. Everything replayable is public: both repositories (github.com/jyh/salt and jyh/saltworks) since 2026-08-16, every theorem replaying with one command; the remaining campaign registers become public at publication; the submitted design’s files are on the shuttle’s public record.

The disclosure block itself deserves reading as a document of its moment, because papers like this are setting the norms the next decade will inherit. The agents are named as Claude-family models (Anthropic), operated under consumer subscriptions; the work is described as a month-long collaboration between the author and Claude; the collaboration is, the acknowledgements note, itself the subject of the paper — the agents’ contributions (the proofs, the designs, the drafts, and the errors caught and corrected) documented in the published registers. Text and figures may carry Anthropic’s content-provenance marks — imperceptible text watermarks, C2PA metadata on images — disclosed rather than scrubbed. A full model and version enumeration is deferred to the pre-publication content freeze, so even the disclosure has a measured scope and a date. And the authorship line is drawn exactly where this lesson’s Chapter 2 would predict: no AI system is an author, because authorship in this method is the reserved human function — statements of results, designs, and rulings — and the author reserves precisely those to himself, taking responsibility for the rest. The fleet did the work; the human owns the claims. That sentence is the paper’s entire authority model, applied one last time to the paper itself.

The regime boundary — when does the inversion hold?

The discussion states the inversion’s domain with care, and it is worth restating as a condition you can test your own work against. The kernel becomes the precondition for productivity when generation is fast, cheap, and fallible — all three. Slow generation (a human mathematician) makes verification a tax again: the checker idles while the generator thinks. Expensive generation changes the budget arithmetic. And infallible generation — if it existed — would need no referee. The 2026 model regime sits squarely inside all three conditions, which is why the paper’s timing is its argument: this inversion was not available in 1992, and the author spent thirty-four years positioned for the day it would be. Whether it holds outside this regime, the paper explicitly does not claim — and its own records mark the edges: the SAT links where the checker frontier ends, the 21-hour ceiling on landing-bearing silence, the measurement gaps the meter’s late window leaves.

Note also how the publication schedule itself is tiered like everything else in the method: the replayable core (both repositories, the ledger) went public first — 2026-08-16, five days after the campaign’s final day; the survey’s evidence ships with the paper; the remaining registers — including the audit briefs about the paper itself — are staged for publication; and the physical artifact arrives on the vendor’s schedule, mid-2027. Nothing is promised as “available on request.” Each artifact class has a date, and the classes most needed for verification shipped earliest — disclosure engineered with the same priority ordering as the fleet’s checkers.

And for readers of this site’s harness-engineering lessons, file the Salt method where it belongs: it is the maximalist answer to the verifier problem every agent harness faces. Evals sample behavior; judges estimate it; this configuration found a domain where the verifier is perfect — and then showed that everything else (scope, provenance, economics, priority) still needs governing, and how. The exportable lesson is not “use Lean”; it is the checker-per-claim-type discipline, the append-only record, the self-serving-direction rule, and budgets that fail loudly — none of which requires a proof kernel to adopt tomorrow.

Three audiences will carry three different things out of this case study, and it is worth naming each exit explicitly. For the formal-methods community: the sixty-year cost objection — their field’s permanent headwind — has an existence proof against it, and the demand curve for kernels, importers (the missing Verilog-to-Lean tool is now a named, valuable gap), and certificate tooling just moved. For AI labs: a working alternative to the eval-and-vibes trust stack — checker-per-claim-type, append-only ledgers, pre-registered instruments — demonstrated at fleet tempo by one user of their consumer products, with the governance doing work their benchmarks cannot. For working engineers: the degraded profile of Chapter 3 — naked-number bans, frozen acceptance criteria, prepared clicks, self-serving-direction burdens — adoptable this sprint, no prover required. The paper is one artifact; its readers’ obligations differ. What none of the three can honestly take away anymore is the old comfort that rigor at speed is impossible.

The transferable core — a closing checklist

Strip the Lean, the sieves, and the silicon away, and what this case study hands any team running AI agents is a short list of load-bearing practices, every one demonstrated under fire in the record you have now read:

None of these requires a proof kernel — the kernel is what made them enforceable at fleet speed in this campaign, and your enforcement will be softer without one. But softer enforcement of the right constitution beats perfect enforcement of none, and the paper’s deepest export is the constitution itself: a working demonstration that autonomy and authority are not opposites — that the way one person safely directs machines working a hundred times faster than they can read is to govern the claims, and let the work run.

And a final honesty about this lesson itself, in the paper’s spirit. Everything you have read here is a certificate: a restatement of the paper’s claims in a simpler vocabulary, at the grades the source states, with the connective tissue labeled ours wherever it is ours. By the certificate contract, you should assume you have been reading something weaker than the full record — the corpus, the registers, the ledger, and the per-claim evidence files all carry more than any lesson can. The implication in this direction is not kernel-checked; no implication between prose documents can be. But the discipline transfers: if a claim in this lesson seems stronger than the paper supports, the paper wins — and the public artifacts, not this page, are the record. Interrogate them; that is what they are for.

Exercises

1. Draft the strike. Your team published an internal benchmark claiming your agent is “3× faster than baseline.” A re-run shows 0.8×–40× across three seeds. Write the retraction entry Salt-style: what is struck, what evidence, what standing law follows. Check: the entry names the instrument and runs, strikes the claim without deleting it, and mints a law about the class (“no speedup ratios from n<N runs / without variance reported”) — not just this instance. Same-day matters: a wrong number’s half-life is measured in citations.

2. Build a priority lane. Design one of the five adversarial search lanes: how do you find prior art published under a different name that no text search could see? Check: you need semantic search over statements (embeddings of formal statements or their informal glosses), plus lanes that walk citation graphs and library dependency graphs — the predecessor that text search misses is found by matching what a theorem says, not what it is called. That the fleet found one this way is quiet evidence the lanes were real.

3. The transfer test. Pick your own domain and name its best available incorruptible checker (compilers: differential testing oracles; protocols: model checkers; data pipelines: reconciliation against source-of-truth). Then write the one-sentence version of each of the three commitments for your domain. Check: if your domain truly has no incorruptible checker, the method’s precondition fails — and the paper honestly would not claim to apply; the pairing of fast generation with incorruptible checking is the whole foundry. Most domains have a weaker checker than a kernel and a stronger one than vibes; the discipline transfers proportionally.

4. The whole paper, in ten graded claims. Close the lesson by writing the paper’s ten most important claims from memory, each tagged with its grade (kernel / instrument / surveyed / confessed). Then check yourself against this row of anchors: zero incorrect proofs in the record (kernel-adjacent: structurally enforced); 73 theorems’ provenance (mechanical, replayable); 288/902 at the measured die (instrument); no ratio for the shipped die (confessed refusal); 29.3% of mathlib (instrument); nine pillars unproved in public (surveyed, as of 2026-08-11); the M₂ wall (kernel); 37h21m floor (instrument, corrected against self-interest); the struck 52× ratio (confessed, preserved); the inversion thesis itself (interpretation, argued from all of the above). Check: if you can produce the list with the grades, you have what this lesson was for — not the numbers, but the habit of never letting a number travel alone.