The first release of the specification bundle since v0.6.6, and unlike 0.6.6.post1 it is a real one: the anchor set moved, and it was adopted before being named here — v0.6.7 AUTHORIZED — adopted by b4dc05e307b8 (2/2 of 3), signed by the human principal and by the roster identity this project's model actor actually holds.
Why the bundle moved
Warrant SPEC v0.4 domain-separates signatures: the signed message is "warrant-sig-v1:" || WarrantID_raw rather than the bare WarrantID. tests/spec_conformance/governance_vectors.json is a signature-bearing fixture, so the construction change moved its bytes and therefore its anchor — which made this a release adoption event under GOV-anchors rather than a code change.
All 50 records in .warrants were re-signed: 45 on the host that holds the claude-fable-5 key, which did not travel to do it, and 5 co-signatures locally. No body changed and no WarrantID moved; both were recomputed rather than assumed.
One signing path, after finding eight
The construction was open-coded in eight places — seven in Python and one in Go — and every one of them was found only because something went red. tools/warrant_sig.py now states it once; all seven Python sites call it, and the Go site holds it as a named constant, since Go cannot import Python.
tests/one_signing_path.py scores nine failures against either prior state — including against the tree from before domain separation existed, where there was no literal to grep for — and fails if a ninth copy appears.
The proof guard checks what the theorems mean
It began as a sorry grep and was shown, in turn, to accept: sorryAx _ true; a modifier-prefixed axiom; a #print axioms syntax override by the audited module itself; comment-blinding via a string literal; a vacuous theorem (: True := trivial); definition gutting, where deleting an inductive constructor leaves the pinned statement unchanged; lossily-pinned string literals that made the genesis hashes swappable; one-line namespace X … end X hiding a declaration; and a self-chosen audit scope taken from a config field nothing compiled from.
It now pins elaborated statements and their transitive definition dependencies computed from the kernel environment, queries axioms by loading compiled modules via Lean.Environment.importModules — data, not elaboration, so the audited module cannot influence the query — derives scope as the complement of a declared core-Lean allowance, and states its guarded set by identity. 36 statement pins, 155 definition pins.
The last of those was found by an external cross-family review: the file walk was os.listdir, not recursive, so proofs/Sub/Evil.lean carrying axiom backdoor : False produced zero problems from every textual layer while the bridge printed PREMISE HOLDS. Chasing it surfaced two holes the reviewer had not named, one of which reopened by path the exact route that once let an audited module override the guard's own axiom query.
The vectors now constrain the oracle
Book I 47/49 and Book II 16/17 conformance vectors are spec-derived — 31 quoted verbatim from Book I §7, the rest hand-computed through a second serializer transcribed from §1.1/§2 — and the generators refuse to write when the oracle disagrees. All 63 hand-derivations agreed with the oracle first try and both files regenerate byte-identically, so no vector changed. What changed is what a green regeneration means: against the previous generators, a new negative control scores 2/9, with seven forgeries passing silently including a forged genesis K.
Also
- Rust no longer answers hostile input with SIGABRT. A deep left spine and a nested-JSON bomb overflowed the stack; they are now Book I §3.6 local faults that cannot be widened into canonical failures. Three fence sites the review had not named needed it too, including the derived
Dropglue — fencingstepalone moved the overflow into cleanup. - A check that prints
FAILURES PRESENTno longer returns 0. The sweep that started withpython -m sigma_glyphfound five more, includinghermes_review.py && git pushpushing on a red gate. impl-go's Book I "coverage" was a hardcoded fixture; it now printsVACUOUSand is dropped from both sides of the tally.- An installed copy no longer accuses itself of failing, and every GitHub Action is pinned to a full commit SHA.
SECURITY-ASSUMPTIONS.md: the residuals as a declared scope boundary rather than scattered prose.
What this release does not claim
tools/test-all.sh is ALL GREEN with zero skips across 18 surfaces, and the cross-repo seam with Warrant is green. But no independent gate reviewed any of it — every reviewer was this model family or an external model run by the same operator. Core Lean is trusted rather than checked; the *Run.lean runners remain unproven-faithful I/O; GUARD_CLAIMS.txt is a review-visibility control, not an authority. SECURITY-ASSUMPTIONS.md carries the rest.