The Calculemus Audit

A correct kernel and a wrong compiler

In 2026 Trail of Bits published a soundness-relevant defect in Lean 4. The function String.Pos.Raw.extract behaved one way under its logical definition — the one the kernel reasons about — and another way in its compiled native implementation. The two disagreed.

The precise shape of the bug is what makes it interesting, and it is worth stating carefully because almost every wrong response to it comes from getting this backwards:

The kernel was not wrong. The compiler was. Lean's trusted core continued to reason correctly; the fast native code it hands work off to did not agree with it.

That distinction determines the blast radius. A proof checked by the kernel was unaffected. The defect was reachable only through the constructs that deliberately step outside the kernel and trust the compiler instead — in Lean, principally native_decide and #eval. It affected every stable release up to and including v4.33.1, and was fixed in v4.34.0-rc1.

For most Lean users this is a footnote: don't use native_decide in work you care about, which was already the received advice. For a system whose entire premise is that a machine — never a language model — decides what is true, it was something else.

A premise that has to be load-bearing

Leibniz is an agentic theorem daemon built on one sentence: LLMs propose; only mechanical checkers decide. Language models generate conjectures and candidate proofs. A Lean kernel, an SMT solver, and a set of exact decision procedures decide whether those are correct. A law is stamped Q.E.D. if and only if a field called kernel_verified is true, and that field is written in exactly one place in the codebase.

The motto is Leibniz's own: Calculemus — "let us calculate." The wager is that a dispute can be settled by computation rather than rhetoric. That wager is only as good as the guarantee that a computation actually happened.

So the Trail of Bits bug posed a specific question. If a proposer could get a proof accepted via native_decide, then kernel_verified would mean compiler-verified — and on an affected toolchain, the compiler could be induced to disagree with the kernel. The premise would be broken not in theory but in a way a published exploit could reach.

An initial review assessed the exposure and reached a reassuring conclusion. It had one limitation, stated plainly in its own handoff: it could not execute anything. No Lean toolchain, no container runtime. Every finding was inference from reading code.

The guard that was never enforced

The audit's first finding was that the system already had the right check and did not run it. An axiom-footprint reader existed. It knew that a legitimate Lean proof closes over at most three canonical axioms:

STD_AXIOMS = frozenset({"propext", "Classical.choice", "Quot.sound"})

Anything else — sorryAx, an admitted lemma, a compiler-trusting axiom — is not a kernel decision. But the reader was not consulted by LeanVerifier.discharge, the sole writer of kernel_verified. The sole writer was never the sole checker.

Read as code, that is a missing call. Executed, it is this: a proof of Fermat's Last Theorem derived from False, routed through the real discharge path on the pinned kernel, came back

kernel_verified = True
trust_tier      = MECHANICAL
gate            = PASS
qed             = Q.E.D.

Nothing in the system objected. That is the difference between an audit that reads and an audit that runs, and it is why the rest of this document exists.

The allowlist that had to replace a denylist

The obvious fix — scan for the axiom Lean.ofReduceBool that native evaluation used to introduce — was already obsolete. Since Lean 4.29, native computation emits a generated axiom named after the theorem it serves (<theorem>._native.native_decide.ax_1), not a fixed name. A denylist naming ofReduceBool is blind to native computation on the very toolchain in use, and stays blind as the naming changes again.

So the check is an allowlist: anything outside the canonical three is a finding. This is the first instance of a pattern that recurs through the whole arc — a guard that enumerates what is bad is defeated by the next thing nobody enumerated.

Nine rounds, and every one of them landed

The repository treats adversarial review as a standing gate rather than a judgment call: a change to the trust surface is attacked before it is believed. Each round below was run against the fix produced by the round before it. Every single one found something.

Two checks that never read proposer syntax

Across nine rounds, two things were never broken. Both work the same way: they do not ask a question the adversary can influence.

A compiled reporter

Rather than parsing Lean source in Python, or reading a printed #print axioms line, the mint compiles the candidate into a Lean module and then runs a separately compiled binary that imports the resulting object file and reads the axiom closure straight out of ConstantInfo data via Lean.collectAxioms. It elaborates no proposer-authored syntax. It takes no declaration name to mis-aim. It was compiled when the image was built, so nothing a proposer later writes can change what it does.

A kernel replay

ADR 0097 recorded the kernel-bypass class — skipKernelTC, unsafe self-loops — as unclosable. That claim turned out to be inferred from repository metadata rather than measured. The actual port of lean4checker to the pinned toolchain was two lines: v4.34 had added a maxRecDepth : USize parameter.

With it vendored, every minted environment is replayed through a bare kernel before its footprint is even read. An axiom closure is never consulted for an environment the kernel would reject.

The class no kernel check can catch

Round 8's finding was the hardest, because nothing in it is a bug. Consider a law whose definitional preamble contains a single line:

notation "False" => True
theorem oops : False := trivial      -- 'oops' does not depend on any axioms

The kernel proved exactly the proposition it was handed. The proof is honest. The axiom closure is not merely clean — it is empty. By the only measure the axiom check applies, this exploit is cleaner than a legitimate proof. There is no axiom to catch, because no axiom was used.

First response: audit the data, and say so

The first answer was deliberately modest. Measurement showed the preamble is written only by operator-authored export scripts — nothing on the proposer path touches it — and that no published law used a meaning-changing construct. So the mechanism became a hash pin: every preamble is fingerprinted, and a change fails the build until a human reviews and re-pins it. A construct lint rides alongside as an authoring aid.

The distinction mattered, because adversarial review found seven working bypasses of that lint. Three were the same mistake: scanning Lean by line position — the lesson an earlier round had already recorded, quoted in the lint's own comments, and then violated two checks later. The pin held regardless, because a hash makes no claim about Lean's grammar.

Second response: ask what the statement denotes

Closing the class properly required a different question. The insight is that a compiled expression has already resolved every notation and every name — so the meaning is readable straight off the object file, with no parser-table diffing and nothing to keep in sync with Lean's grammar.

Before designing anything, the live attack surface was measured. Of eleven candidate attacks, four are refused by Lean itself:

Lean refuses ambiguous shadowing rather than silently preferring the new name — a real part of the trust story that nobody had measured. That left eight live attacks in two classes, and both are visible in the compiled artifact:

A first version of the closing guard refused every declaration that did not land at its own name. That is the right precondition for shadowing and the wrong check — an earlier round had pinned an unclosed namespace as an honest operator shape, and the regression set caught it immediately. A guard that drops real proofs is a defect even when it fails closed.

The daemon was not running the code we had fixed

With the mint hardened, a routine check of the nightly beat's log produced the most consequential finding of the arc — and it had nothing to do with Lean.

The daemon runs itself: a scheduled beat syncs a worktree to the merged mainline and turns capped, journalled cycles against it. The governing decision record states that it "always runs the latest operator-merged code, never a working tree." That was an intention, not a check. When the sync failed, the launcher printed a warning and carried on with whatever code was already there.

On the last of those nights the beat ran pinned four trust-boundary records behind the mainline — missing every fix described above, including the one that closed the demonstrated Q.E.D.-on-False hole — and promulgated a law.

Nothing was published; publication is a separate human act and the queue was held. But a verdict had been minted by a build with a known hole, and nothing said so. The three aborted nights each raised an alarm. The night that ran the wrong code raised none, returned success, and journalled a normal-looking entry.

The fix makes a failed sync abort and alarm, verifies the worktree is actually at the merged commit rather than assuming the sync command worked, alarms on a failed fetch instead of only warning, and records which commit produced each beat.

And a worse bug, found only by running the tests

Writing tests that execute the launcher surfaced a defect that predated the fix entirely. If an ordinary directory sits where the worktree should be, git walks up and operates on the canonical repository instead:

canonical repo branch BEFORE: main
  (checkout in the squatter dir SUCCEEDED)
canonical repo branch AFTER : HEAD

The nightly daemon was one stray directory away from detaching the operator's own working checkout. The first version of the fix did not catch this either — its verification passed, because it too was reading the parent repository's state. Only running the script against a real repository revealed it.

Replacing stored verdicts with measured ones

A kernel_verified flag is only as good as the build that wrote it, and the builds had drifted. Every law in the review queue had been minted under some earlier generation of the guards. Each stored verdict was an unverifiable claim.

So all of them were re-discharged through the current mint — compile, kernel replay, axiom closure, denotation — trusting neither the stored flag, nor the stored Q.E.D., nor the source text.

A green result from a check that cannot go red is worthless, so the sweep was verified in both directions. It discriminates — three distinct axiom footprints across the corpus (43 laws closing over all three canonical axioms, 19 over two, 3 over one), not a constant answer. And it goes red on the same code path:

One incidental result is worth recording. Many queue entries display a statement ending := by sorry, which looks alarming. The sweep confirms it is harmless: the statement is cut at its first top-level := and the real proof appended, so the fragment never reaches the kernel. That had been asserted in prose for a long time; it is now measured across every law, by a reader that inspects kernel data rather than source text.

One residue, and it is not a checker gap

Three classes are closed at the mint. One is open, deliberately, and will not be closed by any amount of kernel checking:

@[irreducible] def Riemann : Prop := True
theorem rh : Riemann := by unfold Riemann; trivial

Every layer behaves honestly. The kernel proves the proposition it is handed. The axiom closure is clean. The denotation reads Riemann — the reporter cannot see through an irreducible definition, and the shape is structurally identical to an honest operator helper.

The structural proof that no diff can separate them is concrete: a real published law's statement legitimately names six of its own preamble constants. Any rule of the form "the statement must not name a preamble-introduced constant" would refuse every honest law in the corpus.

This is a faithfulness question — does the formal statement say what the natural-language claim says? — and it belongs to a different gate, one that has existed since the project's second decision record. It is written down rather than implied, and marked in the test suite rather than omitted.

Five findings that outlast the code

1 · "This cannot be checked" needs the same scrutiny as "this is secure"

Twice, a decision record declared a class unclosable. Both times the reasoning was sound about the wrong activity: it ruled out scanning and concluded nothing could check. The kernel-bypass class fell to a two-line port. The statement-meaning class fell to reading a compiled expression. Humility that has not been measured is just another unverified claim.

2 · The dangerous failures return success

A beat that could not run aborted loudly and was noticed. A beat that ran four records behind returned zero and was invisible. A guard blinded by a lexer desync reported clean. The recurring shape is not the alarm that fires — it is the one that cannot.

3 · Allowlists work; denylists are blind

A denylist naming the axiom native evaluation used to emit was already blind on the toolchain in use. The same logic retired a preamble construct lint in favour of a hash pin, which makes no claim about Lean's grammar and therefore cannot be out-parsed.

4 · The guards that held removed the adversary's ability to answer

Every guard that failed asked a question the adversary could influence: what does this source text say, what did this command print, which name should I look up. The two that never failed do not ask: one reads compiled kernel data, the other re-runs the kernel. When a syntactic guard failed a fourth time, the fix was to refuse the construct rather than parse it better.

5 · A green check proves nothing until it has been shown to go red

Every audit landed here carries its own falsification: mutation controls that must be refused, vacuity assertions that fail if the check examined nothing, and regression tests pinning each historical bypass. The seven bypasses of the preamble lint, the three lexer desyncs, and the stale-code beat are all tests now — because the alternative is a suite that is green because it is empty.

The record, in order

Each record states what was decided, what was measured, and — where it applies — what the record itself got wrong. Corrections are appended rather than edited, so a later reader sees the reasoning as well as the outcome.

Final verification state

The suite reporting zero expected failures is the line that matters. Through most of this work it reported one — the strict marker holding the statement-meaning class open. Deleting that marker to make the suite look clean would have been the defect, not the fix. It is gone because the class closed.

Throughout, five files were never modified: the trust policy, the byte-frozen invariants, the boundary guards, the kernel-writer guards, and the verifier itself. The trust boundary was hardened from outside; it was never renegotiated to make a test pass.