Gate work dominates this estate's wall-clock: on 2026-07-29, 3.9 hours of a
session went to Lean re-elaborating proofs nobody had edited while the audit
phases themselves took about fifteen seconds. --audit-only runs every gate
against the artifacts a previous full run left behind: ~60s against ~1280s.
IT IS SAFE ONLY BECAUSE IT REFUSES.
- It requires every shipped .lean to be BYTE-IDENTICAL to a basis recorded by
a previous full run. Not mtimes: `touch` defeats those, and a stale-artifact
check that fails open is worse than no shortcut at all, because a green
button would then describe a corpus that is no longer on disk.
- The basis is gitignored build state, so a fresh clone cannot inherit
permission to skip compiling.
- The closing banner differs and says in words that the run is not evidence.
selftest-auditonly.sh exercises seven cases: no basis, an edited comment
character, a deleted source, a new source, a missing artifact, a truncated
basis, and — asserted as a PASS — every source's mtime touched with bytes
unchanged, which pins the bytes-not-mtimes decision rather than leaving it
implicit. Negative-tested: with the basis comparison disabled a changed source
is wrongly accepted, exit 0 and zero refusals, so the guard is load-bearing.
A PHASE TERMINATOR, because this broke twice. Every self-test lifts a phase
from check.sh by scanning to the next phase marker. The last phase had no
marker after it, so a lift ran to end-of-file and swallowed whatever was
appended later — first Phase 2c into the axgate lift, then T1's tail into the
binding lift, where it referenced $AUDIT_ONLY and died under `set -u`. Both
surfaced as the BASELINE case failing: a self-test blaming a gate for its own
extraction bug. The phases now end at an explicit sentinel and both lifters
stop there, so nothing appended below can silently become part of the last
phase from a lifter's point of view.
TRUSTED-BASE.md records what an audit-only transcript does and does not
establish, and — because it cost a confusing red run today — that lean-guard's
memory clamp presents as `FAIL: Proofs/<module>` while being a resource
condition, not a broken proof.
Verified green: 8 full button runs (four check.sh, four check-scalar.sh) and 20
self-tests across the four repositories, zero red. One earlier run failed on
the memory clamp because the author ran a test suite concurrently; re-run on a
quiet machine, green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
THE SEAM. This repository is checked by two scripts, and until now neither
asserted anything about the other's scope. check.sh's dead-file gate simply
SKIPPED anything named Scalar*, so a new Proofs/ScalarX.lean was gated by
nothing at all: absent from one manifest by exemption, from the other by
omission, compiled by neither, inventoried by neither. Each button now reads
the other's manifest and requires every shipped proof source to belong to
EXACTLY ONE of them — neither orphaned nor double-claimed, both directions,
plus a phantom check on entries naming files that do not exist. Negative-tested
four ways, including the exact hole this item names.
THE SCALAR BUTTON. Closing the seam exposed it as the estate's weakest link,
having been left behind by every hardening round while the main button gained
five phases. 45 lines to 227:
- source-integrity check over its sources;
- harness-pin verification, so running THIS button alone is protected and not
only running it after check.sh;
- a kernel-side axiom-declaration gate over the compiled artifacts, replacing
a source-text grep that is evadable four ways on v4.30.0-rc2;
- a declaration inventory of ~1880 constants against its own allowlist,
diffed both directions with a count trailer. These 13 modules were the only
part of the proof corpus with no inventory: check.sh Phase 2c named them as
uncovered on every run, and now names the button that covers them instead;
- per-certificate exact-cone assertions replacing `-eq 13` over matching
output lines. A count cannot say WHICH certificate is clean and passes just
as happily if one cone is reported twice.
Every fork-specific fact was read from the existing script rather than assumed:
risc0 and betrusted audit sub_loop1_one_spec where dalek and anza audit
cond_add_l_one_spec, untouched.
THREE BUGS, ONE ROOT CAUSE, all found by the gates rather than by review. Each
reasoned about how a thing is SPELLED instead of what it BELONGS TO, and the
corpus punished each: Proofs/ScalarPackSpec.lean is named like the scalar layer
and owned by the main button.
- the scalar dead-file gate globbed Scalar* and demanded ScalarPackSpec be
scalar-owned. REMOVED rather than special-cased: the seam check tests
membership in exactly one manifest, which is strictly stronger than any
prefix;
- the scalar axiom gate scanned Scalar*.olean, reporting "14 modules" for a
13-module manifest. On a tree where check.sh had not run that artifact is
absent and the button would have failed for a false reason. It now scans
the manifest by membership and fails closed on a missing artifact;
- Phase 2c's driver discovery globbed Inventory*.lean and claimed the other
button's driver, then correctly complained its own manifest lacked those
modules.
This is the family the campaign began with: a source-text axiom grep reasoning
about spelling. Recorded in TRUSTED-BASE.md because it generalises.
Also fixed: the first negative test of the scalar gate's absence check passed
for the wrong reason — the button recompiles before the gate runs, so removing
an artifact merely caused it to be rebuilt. Retested against the lifted phase,
where absence is a persistent condition.
Verified green: 24 runs across the four repositories — four main buttons, four
scalar buttons, and sixteen self-tests — zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Phase 2b asks the kernel whether any AXIOM is declared under Proofs/. Phase 3
pins the cones of the named certificates. Between them sat every other
declaration in the corpus — around three thousand of them — and a helper lemma
quietly acquiring a hash oracle in its cone moved nothing either phase looked
at.
Phase 2c closes that. Ported from ltl-accumulator-verified, where a nine-attack
self-test proved a source-regex enumerator evadable by attributed, private,
indented and `instance` declarations and by a nested-namespace basename
collision. Reading the compiled environment sees what the kernel saw; no name
shape hides. Every constant contributes module, name, kind and full axiom cone,
and the observed set must equal inventory-allowlist.txt exactly in BOTH
directions, with a count trailer so a truncated run cannot pass as an empty
diff.
FOUR THINGS THIS BUILD GOT WRONG, each caught by a check rather than by review:
- The number of inventory drivers is a per-repo FACT, not an assumption.
dalek and anza cannot import their corpus as one environment (Proofs.Basic
and Proofs.ConstSpecs both declare CurveFieldProofs.zero_spec); risc0 and
betrusted have no Proofs.Basic at all. Determined by compiling a probe.
check.sh now DISCOVERS its drivers from the filesystem instead of naming
two, and the generator refuses to split out a module the repo lacks.
- The split let one real declaration hide behind another's entry. Keyed on
name alone, the two zero_specs produced byte-identical records, so 3022
declarations were covered by 3021 allowlist entries. Caught by the count
trailer. Every record now carries its originating module.
- The gate's success line said "single sanctioned axiom", inherited from the
accumulator's policy. This corpus permits NONE. A success message
describing a different rule is how an assertion stops meaning anything.
- selftest-axgate.sh lifted Phase 2b with a range ending at "Phase 3", so
inserting Phase 2c between them made it swallow the new phase and die on
variables only check.sh defines — surfacing as the BASELINE case failing,
a self-test blaming a gate for its own extraction bug. Both self-tests now
stop at the next phase marker whatever it is called, and refuse to run if
they capture more than one phase. The guard is the fix; the range was the
symptom.
WHAT THIS IS NOT, recorded in TRUSTED-BASE.md at the same length as the claim:
- No independent cone walker. The accumulator cross-checks collectAxioms
against a hand-written walker. Ported here it was wrong in BOTH directions
on mathlib's inductive shapes: EdPoint gave [] against the kernel's three
axioms, and once extended, ProjPoint gave three against the kernel's none.
Two implementations disagreeing both ways are a second wrong answer, not a
check. These cones rest on collectAxioms alone.
- Thirteen Proofs/Scalar* modules are inventoried by nothing — the
second-button seam, still open. Phase 2c names every uncovered module on
every run so the omission is visible rather than inferred.
selftest-inventory.sh exercises the shipping gate with six cases, each
asserting a specific diagnostic, including the one that matters: a cone
widened by one oracle while name, module and kind stay put. Negative-tested by
disabling the gate's diff, which turns two cases red including one for the
wrong reason, correctly reported as such.
Verified green: 20 runs across the four repositories (four buttons, four
harness, four inventory, four axgate, four binding self-tests), zero red. The
four check-scalar.sh greens from the preceding sweep stand: that script neither
reads the pin file nor changed.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Every gate this repository has was executed by scripts that nothing pinned.
Round-5 review of the companion SLH-DSA repository stubbed the compiler
wrapper alone and its button printed ALL GREEN in 3.6 seconds over
deliberately destroyed proofs; flipping two guards in the audit driver
disabled every check with the digest byte-identical. Depth of checking is
worth nothing if the thing doing the checking is unbound — and every gate
added this week made that gap more valuable to an attacker, not less.
Phase 0c requires every harness file to match HARNESS.sha256. Two design
points carry the weight:
- WHICH files must be pinned is POLICY and lives in check.sh, never in the
map being consulted. If the required set were read from the pin file,
deleting an entry would silently un-pin that file. It is instead derived
from the filesystem, so a deleted entry is a set mismatch and a build
failure. That is the exact defect SLH-DSA round-6 found, closed here by
construction.
- Membership self-derives from the executable bit: anything this script can
shell out to must be pinned, so a NEW script fails closed until someone
pins it deliberately. Load-bearing files that are not executable — the
audit driver, the committed manifests, the policy tables — cannot be
discovered that way and are listed explicitly.
lean-guard is inside the set, which finally makes the standing "lean-guard
stays hash-pinned" rule a property of the repository rather than a convention.
selftest-harness.sh replays five cases, each asserting a specific diagnostic:
an edited lean-guard, a new unpinned executable, a deleted pin entry, a
missing pin file, and a positive control. It was itself negative-tested — with
the hash comparison removed it goes red on exactly that case while cheerfully
reporting "10 harness files match their pins".
TRUSTED-BASE.md states the limit at equal length to the claim: pinning a
harness from inside that harness is circular, and an author who edits a script
and refreshes its pin in the same commit passes every phase. What the pin
changes is that the edit can no longer be SILENT — it must appear in the diff
at the commit being reviewed. A green button says "this is the apparatus that
was reviewed", never "this apparatus is trustworthy".
Also fixed, found by this sweep: both self-tests compared the working tree
against its starting state with `diff <(echo "$VAR") <(command)`, which is
asymmetric — for a clean tree the variable is empty and `echo` emits a blank
line the command does not. It reported a difference precisely when nothing was
wrong, and only surfaced once P1-a was committed and Proofs/ became clean.
Both now compare as strings.
Verified green: 20 runs across the four ed25519 repositories (four buttons,
four harness self-tests, four axiom-gate self-tests, four binding self-tests,
four scalar buttons), zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Phases 3/3b establish what each certificate RESTS ON. Neither says what it
SAYS, nor what it is ABOUT. A certificate gutted to a tautology of the same
axiom cone passes both; so does one whose reference definition has been
redefined to BE the extracted code, at which point the theorem reads
`loop = loop` and every cone is byte-identical.
Phase 3c closes that. Proofs/Audit.lean emits a canonical block holding the
policy constants, every certificate's fully-elaborated statement (pp.all, so
implicit arguments, instances and universe levels are visible), and the body
of every specification constant transitively reachable from those statements.
Its SHA-256 is pinned in check.sh and the block itself is committed as
AUDIT-MANIFEST.txt, so a mismatch is DIFFED, not merely reported. 31
certificates, 68 specification constants per repository.
Two tiers, not one. These forks have an arithmetic tier that must stay
oracle-free and an apex tier carrying this fork's hash and wire-format axioms,
and the apex boundary genuinely differs per fork (dalek 8 extra names, anza 4,
risc0 and betrusted 5). One shared constant would have widened the arithmetic
tier to accept hash oracles, which is the most valuable property these repos
have. Each auditor is generated from its own repository's policy.
Phase 0b pins the extracted model. This was not a precaution: risc0 and
betrusted were observed emitting BYTE-IDENTICAL audit-manifest digests
(6c821b8e…) while shipping demonstrably different extracted models, their
point-doubling routines differing in operation order. A statement names an
extracted function; it does not contain that function's body. Binding
statements is not binding the subject. Membership derives from the filesystem,
so a new model file fails closed.
selftest-statements.sh attacks both phases with ten cases, each asserting a
specific diagnostic: an edited model body, an unlisted model file, a widened
policy, a hand-edited committed block, a certificate dropped from the auditor
WITH the digest refreshed to match, and a gutted statement whose cone is
unchanged. It lifts the phases out of check.sh at run time, so it attacks the
shipping gate rather than a copy.
Two bugs found and fixed during that testing, both mine: Phase 3c read `$0`
after `cd "$AENEAS_LEAN"`, and $0 is the caller's relative path; and the
axgate self-test compared the tree against a pristine checkout rather than
against how it found it. A third expectation was wrong rather than the code —
widening the apex boundary is caught by the exact-cone requirement before the
digest ever runs, which is a stronger rejection, and the test now says so.
All sixteen runs green at these commits: four main buttons, four axgate
self-tests, four binding self-tests, four scalar buttons.
TRUSTED-BASE.md records what this binds and, at equal length, what it does
not: a digest binds identity, not meaning; an author can rotate the pins in
one commit and is caught by review, not by the script; and pinning the model
says nothing about whether Charon and Aeneas translated the Rust faithfully.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Adds one item naming what check.sh Phase 2b binds — every compiled
Proofs/*.olean, kernel-side, membership self-derived, fail-closed on a
missing module — and, more importantly, what it still does not bind:
declarations, not statements. A theorem gutted to a tautology with the same
axiom cone passes every phase. Reading the statements remains a human act,
and this document is where that has to be said rather than left for a
reviewer to discover.
Verified green at this commit's parent across all eight buttons on
2026-07-28; see formal-verification-control/RECORDED-RUN-2026-07-28.md.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- README: pyramid-diagram apex row upgraded to the proven full lift
(accepted <=> decompress(R) = [k](-A)+[s]B), status table names all
four button-enforced tiers, apex section gains the phase-2 tier table
(half-lift / point equation / full lift) + the decompress-chain
summary; source pin updated to the pushed patch commit.
- TRUSTED-BASE item 5: rewritten from the single byte-apex certificate
to the FOUR enforced tiers (decompress_of_canonical noted as
standard-three-only).
- gen/CurveField/FunsExternal.lean: stale root-namespace
edwards.decompress.step_1/step_2 axioms removed (dead weight left
behind by un-opaquing; outside every cone, but they forced
fully-qualified unfolds - see control FAILURES.md).
- check.sh Phase 3b success echo aligned to "apex + full-lift" (echo
only; the enforcing greps covered all four tiers already).
Validated by the pass-4 sweep: 9/9 buttons green (this repo's check.sh
+ check-scalar.sh among them), logs retained in the pass workspace.
Full record: formal-verification-control/COHERENCE-PASS-4.md.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
- README: the pyramid diagram claimed the cofactored ZIP-215 equation,
which is NOT the proven statement - corrected to the actual theorem
(accepted IFF compress([s]B-[k]A) = R, byte-for-byte) and the signature
row now names verify_accepts_iff; new "The signature apex (phase 1)"
section states the theorem, this repo's glue architecture, the exact
button-enforced axiom cone, and the phase-2 deferral.
- TRUSTED-BASE: item 5 rewritten from an aspirational hash paragraph to
the structural boundary - certificate name, exact allowed cone, and the
Phase 3b enforcement that fails the build on any deviation.
- Dead pre-merge artifacts removed: gen/CurveScalar, CurveScalar.llbc,
extract-scalar.sh (the merged gen/CurveField universe is the single
model; check-scalar.sh remains the scalar button, header updated).
- lean-guard: Guard 3a retry ladder (LEAN_MEM_WAIT_SEC) - a clamped run
that dies on memory retries as headroom improves, converting ambient
memory pressure from a deterministic abort into a delayed pass.
Fresh green buttons after these changes: check.sh (incl. Phase 3b apex
audit) + check-scalar.sh, both at shipped defaults, coherence pass 3
sweep 2026-07-05.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
