hyperpolymath · Nov 9, 2026 · Nov 9, 2026 · Nov 9, 2026 · Nov 9, 2026 · Nov 9, 2026
diff --git a/CLAUDE.md b/CLAUDE.md
@@ -18,7 +18,7 @@ Guidelines and context for working with Claude Code on the ECHIDNA project.
 - **RSR / CCCP compliance statement**: [`RSR_COMPLIANCE.adoc`](RSR_COMPLIANCE.adoc)
 - **Proof and verification policy (normative)**: `3-practice/PROOF-POLICY.adoc`
   in [hyperpolymath/standards](https://github.com/hyperpolymath/standards) —
-  which prover carries which obligation (Rust→Creusot, Ada→SPARK,
+  which prover carries which obligation (Rust→Creusot with Pearlite, and Verus (§1.2); Ada→SPARK,
   APIs/ABIs→Idris 2, theory→Agda rechecked in Rocq and Lean), and the closed
   status vocabulary (`proven`, `proven-with-postulates`, `tested-only`,
   `argued`, `open`). A change to the mapping is an owner ruling and requires

diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc
@@ -62,45 +62,49 @@ CI gate exists and the authors say it passes" when no receipt is cited.
 |Not done.
 |===
 
-=== Relation to the Mathesis grades
+=== Relation to the Proof Witness Grades (PWG)
 
-https://github.com/hyperpolymath/mathesis[mathesis], *Estate-wide Mathematical
-Knowledge Architecture* §5, grades a *theorem* by how far its witness has
-travelled: **Grade 3** type-checks locally in its home system and is not
-translated; **Grade 2i/2ii** one / two independent translations with statement
-correspondence recorded; **Grade 1** machine-checked through a verified checker
-API in headless CI.
+`+PROOF-POLICY+` §8 (owner ruling 2026-11-04) is normative for grades. A PWG
+says how many independent machine-checked witnesses a *theory* theorem has:
+`+PWG-3+` (Agda source checked under the §2.1 invocation, with a receipt),
+`+PWG-2i+` (plus one counted Rocq or Lean leg), `+PWG-2ii+` (plus both),
+`+PWG-1+` (every counted witness has a current per-commit receipt from a
+headless, isolated, pinned run). Always write the `+PWG-+` prefix.
 
-The two vocabularies are orthogonal — one grades a theorem's reach, the other
-records whether a repository's obligation was discharged — but they interact:
+* *Engineering proofs are not graded* (§8.1). Creusot, Verus, SPARK and Idris 2
+  results, and Agda statements about ECHIDNA's own functions and types, use the
+  §5 tokens only. In this file that covers R1, R2, R3, R9, R10, R12 and most of
+  R4. A theory theorem below `+PWG-3+` is `+ungraded+`.
+* A recheck leg counts only when its kernel accepted it *and* its §2.2
+  correspondence is `+RECONCILED+`. Until then it is not a witness.
 
-* A home-system leg may be `+proven+` while every independent leg is `+open+`.
-  That combination *is* Grade 3, and it is the ceiling for anything in this
-  repository.
-* A translation leg is `+argued+`, not `+proven+`, until the statement
-  correspondence is recorded (`+PROOF-POLICY+` §2: "`the kernel checks the term
-  only against the translated statement`").
-
-Mathesis §6 forbids flattening assurance into a percentage. See R5 and R6.
+Grades are derived from receipts, never asserted, and are never flattened into
+a percentage. See R5 and R6.
 
 == Obligations
 
 Grouped by the `+PROOF-POLICY+` §1 mapping, because that is what decides which
 verifier is even allowed to carry the row.
 
-=== Rust — Creusot (§1: first-party Rust)
+=== Rust — Creusot, Pearlite and Verus (§1, §1.2: first-party Rust)
 
 [width="100%",cols="24%,13%,38%,25%",options="header"]
 |===
 |Obligation |Row |Basis |Evidence / next step
 
 |R1. Trust pipeline, dispatch, arbitration, Pareto
 |`+open+`
-|`+PROOF-POLICY+` §1 maps first-party Rust to Creusot.
-|`+crates/echidna-core-creusot+` describes itself as "`Creusot-annotated (not
-yet proved)`"; the `+creusot+` dev-dependency is commented out and the crate
-builds on stable Rust behind a `+creusot+` feature. Annotation is not proof. Row
-stays `+open+` until a Creusot run yields a receipt with a commit hash.
+|`+PROOF-POLICY+` §1 maps first-party Rust to Creusot with Pearlite contracts,
+and Verus (§1.2, owner ruling 2026-11-07: the default Rust toolset).
+|*Creusot:* `+crates/echidna-core-creusot+` describes itself as
+"`Creusot-annotated (not yet proved)`"; the `+creusot+` dev-dependency is
+commented out and the crate builds on stable Rust behind a `+creusot+` feature.
+Annotation is not proof. It is also a *parallel model* ("`NOT a runtime
+dependency`"), so even a green Creusot run would cover that model, not the
+shipped `+src/rust/+` code, until a refinement or the annotations move onto the
+shipped code. *Verus:* not started; no Verus specification or proof exists.
+Row stays `+open+` until a Creusot or Verus run on shipped code yields a receipt
+with a commit hash.
 
 |===
 
@@ -118,13 +122,32 @@ ABI row and the Stage-8a trio as constructively proved, all in
 
 |R2. Idris 2 interface/ABI obligations (E2, E3, E5, E6, E7, E12, Stage 8a,
 VQL-UT, extensive ABI)
-|`+argued+`
+|`+proven+`
 |`+PROOF-POLICY+` §1 maps ABIs and engineering properties to Idris 2. The
 artefacts exist and are detailed in `+PROOF-NEEDS+`.
-|No `+idris2 --build+` receipt for
-`+verification/proofs/idris2/echidna-verif-proofs.ipkg+` is cited with a commit
-hash. Promote to `+proven+` by citing a green run and its commit — that is a
-one-line change, and it is the cheapest upgrade in this file.
+|*Receipts (2026-11-09).* CI runs on commit
+`+a2a8643b1b96bb33519950586375c07e3fa12f96+`, whose `+verification/+` and
+`+src/abi/+` trees are byte-identical to `+main+` `+2ab7574+` (checked with
+`+git diff+`):
+https://github.com/hyperpolymath/echidna/actions/runs/42624461538/job/129184535654[Idris2 (verification)]
+builds `+verification/proofs/idris2/echidna-verif-proofs.ipkg+` and
+https://github.com/hyperpolymath/echidna/actions/runs/42624461712/job/129184533713[Type-check Idris2 ABI definitions]
+builds `+src/abi/echidnaabi.ipkg+`, both on Idris 2 0.8.0, both success.
+`+%default total+`. A 2026-11-09 audit of both packages found no `+believe_me+`,
+`+assert_total+` or `+postulate+` declarations (the only textual hits are a
+doc comment and the pattern strings in `+AxiomCompleteness.idr+`). That is a
+receipt-time audit, not an enforced property: `+idris2-abi-ci.yml+` greps
+`+src/abi/+` only, for `+believe_me+`, `+assert_total+`, `+unsafePerformIO+`
+and `+prim__crash+`, and checks neither `+postulate+` nor
+`+verification/proofs/idris2/+`. *Limit:* `+EchidnaABI.CapnSchemas+` was
+outside the package and failed to build; hyperpolymath/echidna#472 fixes it and
+gates it. Nine other `+.idr+` files at the `+src/abi/+` root are outside the
+package: `+BojForeign+`, `+OverlayForeign+`, `+TentaclesForeign+`,
+`+TypeLLForeign+`, `+Types+`, `+Layout+` and `+Foreign+` (shadow copies of
+packaged modules), `+CoprocessorForeign+` (an orphan whose module name does not
+match its path) and `+NeSyAssistTesting+` (does not parse, and states an
+empirical claim rather than a provable one). They carry no row until the owner
+decides their fate (open question A5).
 
 |===
 
@@ -137,15 +160,41 @@ one-line change, and it is the cheapest upgrade in this file.
 |R3. Lean 4 legs: E4-L4 `+ConfidenceLattice.lean+`, E10
 `+ParetoMaximality.lean+` / `+ParetoStrongMaximality.lean+`, E11
 `+IntegrityVerification.lean+`, E13 `+PortfolioCompleteness.lean+`
+|`+open+` (the Lean build passes; the verifier placement is unresolved)
+|*Corrected 2026-11-09.* The 2026-05-18 record (all five failing) is stale.
+https://github.com/hyperpolymath/echidna/actions/runs/42624461538/job/129184535185[Lean 4 (verification)]
+builds all five with `+lake build+` on the pinned `+lean-toolchain+` (4.13.0),
+success, on commit `+a2a8643+` (tree identical to `+main+` `+2ab7574+`). A
+2026-11-09 audit run of `+#print axioms+` over 77 of the 79 theorems found only
+`+propext+`, `+Quot.sound+` and `+Classical.choice+` — no `+sorryAx+`.
+|*Placement is still open.* These statements are about ECHIDNA's own types
+(confidence lattice, Pareto order, integrity, portfolio), so §1 assigns them
+to Idris 2 (or Creusot/Verus on the Rust), not Lean. Calling them "§4
+exceptions" is not enough: no §4 exception record (reason, alternative
+considered) exists beside them. Owner call: write the §4 records, or move the
+statements to Idris 2. Being engineering proofs, they carry no PWG (§8.1).
+
+|===
+
+=== Ada — SPARK (§1: first-party Ada)
+
+[width="100%",cols="24%,13%,38%,25%",options="header"]
+|===
+|Obligation |Row |Basis |Evidence / next step
+
+|R12. SPARK projects: `+src/ada/spark/echidna_spark.gpr+`,
+`+spark/axiom_tracker+`, `+spark/certificates+`, `+spark/solver_integrity+`
 |`+open+`
-|Directly recorded: `+lake build+` run 2026-05-18 (Lean 4.13.0) — *all five
-fail to compile*, 49 / 2 / 1 / 5 / 31 errors, three root causes
-(`+unfold_let+` removed in 4.13.0; Mathlib tactics under a zero-mathlib
-lakefile; instance synthesis and module resolution).
-|Nothing. This row is correct and must not be softened. `+PROOF-NEEDS+` records
-that `+ConfidenceLattice.lean+` was left byte-identical and that the
-`+unfold_let+` token-swap made it worse (104 errors). The open decision is
-Mathlib-vs-core, which is an owner call.
+|`+PROOF-POLICY+` §1 maps Ada to SPARK. Four GPR projects exist; this row was
+missing from the file until 2026-11-09.
+|No `+gnatprove+` receipt exists. No workflow runs `+gnatprove+`; the only
+recipe (`+Justfile+`, `+gnatprove -P src/ada/spark/echidna_spark.gpr+`) covers
+one of the four projects and is not run in CI. *Boundary, recorded:*
+`+Axiom_C_Bridge+` (`+src/ada/spark/axiom_c_bridge.ads:23+`, `+.adb:16+`) is
+`+SPARK_Mode => Off+` — the C-ABI seam — so it is outside any SPARK proof and is
+an `+ASSUMED+` boundary for anything that calls through it. Next step: a pinned
+`+gnatprove+` job over all four projects, or a §6 toolchain deviation recorded
+here.
 
 |===
 
@@ -260,7 +309,7 @@ Rocq/Lean rechecks and statement correspondence also remain open in R5.
 |`+open+`
 |`+PROOF-POLICY+` §2: every Agda theory proof is rechecked in both, transported
 through Dedukti or re-proved, with the route recorded per theorem.
-|Never attempted. This is what holds the set at Mathesis *Grade 3*: locally
+|Never attempted. This is what holds the theory set at `+PWG-3+`: locally
 checked, untranslated. ECHIDNA's `+src/rust/exchange/+` speaks Dedukti, so the
 transport route exists; using it is unstarted work, not a missing capability.
 
@@ -351,13 +400,15 @@ mean "ECHIDNA is verified" — it would mean one named obligation was discharged
 by one named tool with its boundary written down. Nothing here vouches for a
 prover backend's own soundness.
 
-Four rows are `+proven+` today — R4, R9, R10, R11 — and each names the kernel,
-the flags and the limit that qualify it (R4 carries the
-`+UnsupportedIndexedMatch+` caveat, R9 the digest-level scope). Every *independent*
-leg is still `+open+`: R5 has never been attempted, which is why the corpus sits
-at Mathesis Grade 3 and not above it. Those two facts are not in tension —
-proven in one kernel is exactly what Grade 3 means — and neither of them is an
-omission.
+The `+proven+` rows — R2, R4, R9, R10, R11 — each name the kernel, the
+receipt and the limit that qualify them (R2 the receipt-time escape-hatch
+audit, R4 the `+UnsupportedIndexedMatch+` caveat, R9 the digest-level scope).
+R3 stays `+open+`: its Lean build passes, but Lean is not the verifier §1
+assigns to those statements until the placement is decided. Only theory theorems are graded (§8.1): R11 is at
+`+PWG-3+`; the engineering rows carry no PWG. Every *independent* leg is still
+`+open+`: R5 has never been attempted, which is why nothing here is above
+`+PWG-3+`. Proven in one kernel is exactly what `+PWG-3+` means, and neither fact
+is an omission.
 
 == Related