diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
index 488532b..15f0f71 100644
--- a/.machine_readable/6a2/STATE.a2ml
+++ b/.machine_readable/6a2/STATE.a2ml
@@ -6,9 +6,9 @@
 [metadata]
 project = "typed-wasm"
 version = "0.1.0"
-last-updated = "2026-05-25"
+last-updated = "2026-05-27"
 status = "active"  # active | paused | archived
-session = "2026-05-24/25 — Phase 0 closure pass. 11 PRs landed (#46 CI triage, #47 PRODUCTION-PATH doc, #55 cargo-audit CI, #57 Track C complete +64 assertions and 2 real bugs fixed, #58 tree-sitter scaffold, #59 CI hardening non-blocking, #60 ROADMAP truthfulness audit + drift-detection aspect §8, #61 wiki source-of-truth + STATE.a2ml comprehensive, #62 tree-sitter v1 parses example 01 end-to-end with 0 ERROR, #63 repo tidy RSR-aligned + smoke fix + duplication scrub). Phase 0 gates 1 + 3 met; gate 2 (codegen v0) is the terminal Phase-1-handoff item."
+session = "2026-05-27 — Proof-debt closure pass.  3 PRs auto-merge SQUASH armed: #79 (TypedWasm.ABI.VerifierSpec, total bodies for VerifierSpecAgreement / SourceVerifierAgreement closing post-A10 items 7 + 8 — design: VADifferential / SADifferential carry inline TrustedFixture so the structural witness travels with fixture metadata, making all four agreement directions total by case analysis; first total no-believe_me agreement values in the codebase); #80 (Proofs.idr LevelAttestationW + WitnessCertificate closing standards#130 long-tail flagged in PROOF-NEEDS 2026-05-18 reconciliation banner — design: 15-ctor witness-indexed GADT with per-level extractors discharging the 'attestation entails the level's semantic property' claim, plus existential SomeAttestationW wrapper enabling WitnessCertificate as the heterogeneous-list lift of ProofCertificate); PR #83 (the second slice) instant-merged into #80's branch because the stacked base wasn't protected, so #80's squashed commit carries both slices.  #74 closed as superseded by #79 (competing Maybe-bridge design replaced by witness-carrying ctor design).  PRs #76 / #77 (verifier L1-L6 carrier section proposal + L2 codec pre-staging) IN PROGRESS by a parallel session — left untouched per parallel-session policy.  Test surface 545 → 627+ assertions (proof regression 25 → 107).  Previous session 2026-05-24/25 = Phase 0 closure pass (11 PRs landed, gates 1 + 3 met; gate 2 codegen v0 is the Phase-1-handoff item)."
 
 [project-context]
 name = "typed-wasm"
@@ -51,6 +51,9 @@ milestones = [
   { name = "Wiki source-of-truth at docs/wiki/", completion = 100 },  # 2026-05-25 (PR #61)
   { name = "RSR-template taxonomy alignment (AUDIT.adoc + onboarding/status/proposals stubs)", completion = 100 },  # 2026-05-25 (PR #63)
   { name = "Parser migration ReScript -> AffineScript -> Idris2", completion = 50 },  # ReScript->AffineScript landed; AffineScript->Idris2 still ahead
+  { name = "VerifierSpecAgreement / SourceVerifierAgreement bodies (post-A10 items 7 + 8)", completion = 100 },  # 2026-05-27 (PR #79, auto-merge armed)
+  { name = "LevelAttestation reindexed-by-witness (standards#130 long-tail)", completion = 100 },  # 2026-05-27 (PR #80, auto-merge armed)
+  { name = "WitnessCertificate lift (heterogeneous-list certificate)", completion = 100 },  # 2026-05-27 (#83 folded into #80)
 ]
 
 [blockers-and-issues]
@@ -79,16 +82,40 @@ actions = [
   "ADRs for the 6 load-bearing decisions D1-D6 from docs/PRODUCTION-PATH.adoc §'Load-bearing decisions' (especially D2: producer-side-only vs runtime-aware, which gates whether Phase 3 happens).",
 ]
 
+[proof-debt-closure-pass-2026-05-27]
+# Snapshot of the 2026-05-27 proof-debt closure pass.  Three PRs auto-merge
+# SQUASH armed at the time of writing.  When all three land, this section
+# can move to history (or be summarised in the session note).
+prs = [
+  { number = 79, title = "VerifierSpec.idr — total bodies for VerifierSpecAgreement + SourceVerifierAgreement (items 7 + 8)", state = "open-auto-merge-armed", branch = "proof/verifier-spec-agreement-bodies", closes-audit-items = ["7", "8"], lines-added = 670, new-regression-assertions = 33 },
+  { number = 80, title = "LevelAttestationW + WitnessCertificate (standards#130 long-tail)",                               state = "open-auto-merge-armed", branch = "proof/level-attestation-witness-indexed", closes-audit-items = ["standards#130 stronger reindexed claim"], lines-added = 828, new-regression-assertions = 49 },
+  { number = 74, title = "items 7+8 design pass + Maybe-returning bridges (superseded by #79)",                            state = "closed", reason = "superseded — competing design with weaker provability of the agreement records" },
+]
+test-surface-delta = "proof regression 25 → 107 (+82); total 545 → 627+"
+banned-pattern-delta = "zero new (believe_me/assert_total/postulate/sorry/assert_smaller); %default total preserved"
+build-oracle = "IDRIS2_PREFIX=…/idris2/0.8.0 idris2 --build src/abi/typed-wasm.ipkg → 22/22 modules under #79, 21/21 under #80, rc=0"
+
+[long-tail-open-after-2026-05-27]
+items = [
+  "WasmCert-Isabelle tie-back (requires external Isabelle/HOL install + bridge — multi-week)",
+  "Emitted-wasm byte-equality P3.1(a) — blocked on .twasm→.wasm emitter not yet existing",
+  "Parser round-trip in Idris2 — blocked on AffineScript parser port to Idris2",
+  "Verifier L1-L6 + L13-L16 coverage on emitted wasm (#34, #35) — IN PROGRESS on PRs #76 / #77 by a parallel session, do not interfere",
+]
+
 [maintenance-status]
-last-run-utc = "2026-05-25T20:00:00Z"
+last-run-utc = "2026-05-27T10:30:00Z"
 last-report = "docs/PRODUCTION-PATH.adoc"   # the canonical strategic doc supersedes one-off audit reports
 last-result = "pass"  # unknown | pass | warn | fail
 open-warnings = 4  # Build+E2E + A2ML + K9 non-blocking advisories (PR #59) + anti-pattern policy (fixed by Track A's ReScript cut)
 open-failures = 0  # all gating CI is green; previously-red jobs are explicitly advisory now
 
 [test-surface]
-# Test surface as of 2026-05-24; ~545 assertions across 11 surfaces.
-total-assertions = 545
+# Test surface as of 2026-05-27; ~627 assertions across 11 surfaces.
+# Proof regression jumped 25 → 107 in the 2026-05-27 proof-debt closure
+# pass: +33 from PR #79 (VerifierSpec) and +49 from PR #80
+# (LevelAttestationW + WitnessCertificate).
+total-assertions = 627
 surfaces = [
   { name = "ParserTests.res",                 assertions = 88,  file = "tests/parser/ParserTests.res" },
   { name = "typed-wasm-verify (Rust)",        assertions = 53,  file = "crates/typed-wasm-verify/" },        # 43 unit + 10 cross-compat
@@ -96,7 +123,7 @@ surfaces = [
   { name = "claim-envelope aspect",           assertions = 53,  file = "tests/aspect/claim-envelope.mjs" }, # bumped 49→53 in PR #60 (new section 8 drift detection)
   { name = "security-envelope aspect",        assertions = 10,  file = "tests/aspect/security-envelope.mjs" },  # added 2026-05-24 (PR #57)
   { name = "property tests",                  assertions = 29,  file = "tests/property/property_test.mjs" }, # added 2026-05-24 (PR #57)
-  { name = "proof regression",                assertions = 25,  file = "tests/proof/regression.mjs" },        # added 2026-05-24 (PR #57)
+  { name = "proof regression",                assertions = 107, file = "tests/proof/regression.mjs" },        # 25 from PR #57, +33 from PR #79 (VerifierSpec), +49 from PR #80 (LevelAttestationW + WitnessCertificate) — all 2026-05-27
   { name = "smoke E2E",                       assertions = 40,  file = "tests/smoke/e2e-smoke.mjs" },
   { name = "structural E2E",                  assertions = 53,  file = "tests/e2e.sh" },
   { name = "integration (airborne-step)",     assertions = 14,  file = "tests/contracts/airborne-step-state-contract.mjs" },
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 4647415..ff87477 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -10,6 +10,82 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Proof-debt closure pass (2026-05-27)
+
+Post-Phase-0 sweep of the long-tail items the 2026-05-18 PROOF-NEEDS
+reconciliation banner deferred. Closes the named obligations against
+post-A10 audit items 7 + 8 (verifier ↔ spec, source ↔ verifier
+agreement records) and the standards#130 "LevelAttestation reindexed
+by witness" long-tail. All work additive (no existing definitions
+touched, no prior proofs can regress) and all changes preserve
+`%default total` with zero new `believe_me` / `assert_total` /
+`postulate` / `sorry` / `assert_smaller`.
+
+**3 PRs landed/in flight, all auto-merge SQUASH armed**:
+
+- **#79** — `TypedWasm.ABI.VerifierSpec`: total bodies for
+  `VerifierSpecAgreement` and `SourceVerifierAgreement` (post-A10
+  audit items 7 + 8). New module (~620 LOC) defining the shared
+  spec-of-record surface (`ModuleSummary` / `FunctionSummary` /
+  `OwnershipIntent`), structural acceptance predicates
+  (`TokenFresh` / `IntentsLinearAcceptable` / `FunctionsAccepted`),
+  three acceptance predicates (`SpecAccepts`, `VerifierAccepts`,
+  `SourceAccepts`), the two agreement records with totally-proven
+  bodies, and concrete inhabitants `verifierSpecAgreement` /
+  `sourceVerifierAgreement` (the first total no-`believe_me`
+  agreement values in the codebase). Design choice that unblocked
+  the bodies: `VADifferential` / `SADifferential` carry an inline
+  `TrustedFixture` so the structural witness travels with the
+  fixture metadata — trust-injection moment moves to
+  `MkTrustedFixture` (single audit grep). End-to-end demo through
+  `fixtureCleanLinearConsumerModule` (cross_compat row 1).
+  Discrimination proofs across both ctors show L10 has teeth and
+  the differential escape hatch can't smuggle a bad module past
+  the verifier. **+33 Layer 1 regression assertions.**
+  Side-fix: latent `idris2 --check typed-wasm.ipkg` bug in
+  `regression.mjs` Layer 2 corrected to `--build` (Idris2 0.8.0
+  `--check` rejects ipkg paths; CI was unaffected because Layer 2
+  skips when idris2 not on PATH, but local strict runs failed).
+- **#74** — closed as superseded by #79 (competing `Maybe`-returning
+  bridge design; the witness-carrying ctor design in #79 closes the
+  full bodies that #74's design explicitly framed as "multi-week
+  residual").
+- **#80** — `Proofs.idr` `LevelAttestationW` + `WitnessCertificate`:
+  closes the standards#130 long-tail flagged in PROOF-NEEDS
+  2026-05-18 reconciliation banner ("Stronger 'attestation entails
+  the level's semantic property' (needs `LevelAttestation` reindexed
+  by witness) remains tracked future work under standards#130").
+  Two stacked slices (PR #83 instant-merged into #80's branch
+  because the stacked base wasn't protected; the squashed commit
+  carries both):
+    - **`LevelAttestationW : (n : Nat) -> Type`** — witness-indexed
+      attestation GADT, one constructor per level (15 total). Each
+      packages the level-specific witness. 15 `attestLNW_*` smart
+      ctors. 15 `attestLNW_Entails<Property>` extractors (the
+      "entails-semantic-property" lemmas). `toLegacy` bridge. 15
+      round-trip `Refl`s. Uniform `attestLW_AchievedIn` subsuming
+      the A9 `attestLN_Sound` family.
+    - **`WitnessCertificate`** — `ProofCertificate` lifted to
+      witness-carrying form via existential `SomeAttestationW`.
+      Mirror record. `witnessToLegacy` bridge. `composeWitness`
+      mirror of `composeCertificates`. `composeWitnessLegacyAgree`
+      composition-compat lemma. `WitnessAchieved` predicate lifted.
+      Empty + singleton smart ctors.
+  **+49 Layer 1 regression assertions.**
+
+**Test surface after this pass**: 627+ assertions (up from 545+).
+Per-surface delta: proof regression 25 → 107 (33 from #79 + 49 from
+#80, plus the existing 25).
+
+**What this does NOT close**:
+
+- WasmCert-Isabelle tie-back (requires external Isabelle install)
+- Emitted-wasm byte-equality, P3.1(a) (blocked on `.twasm`→`.wasm`
+  emitter)
+- Parser round-trip in Idris2 (blocked on AffineScript parser port)
+- Verifier L1–L6 + L13–L16 coverage (in progress on PRs #76 / #77 in
+  a parallel session — wire-format proposal + L2 codec pre-staging)
+
 ### Phase 0 closure pass (2026-05-24 / 2026-05-25)
 
 Two sessions of focused engineering-surface stabilisation, closing the
diff --git a/LEVEL-STATUS.md b/LEVEL-STATUS.md
index 10c5f5c..36fe3f4 100644
--- a/LEVEL-STATUS.md
+++ b/LEVEL-STATUS.md
@@ -101,10 +101,11 @@ toolchain remains future work.
 | SessionProtocol.idr | 0 | 0 | 0 | In package (v1.3 / L14) |
 | ResourceCapabilities.idr | 0 | 0 | 0 | In package (v1.4 / L15) |
 | Choreography.idr | 0 | 0 | 0 | In package (v1.5 / L16) |
-| Proofs.idr | 0 | 0 | 0 | In package.  Attestation API hardened A7 (2026-04-18): every L1-L10 attestation now requires a witness from its level module (Schema / FieldIn / WasmTypeCompat / Ptr-NonNull / InBounds / AccessResult / ExclusiveWitness / EffectSubsumes / Lifetime.Outlives / CompletedProtocol).  `simpleReadCert` / `fullCert12` / `fullCert15` thread witnesses per level; the certificate cannot be constructed without real proof artefacts.  Level-achievement layer added A8 (2026-04-18): `LevelAchievedIn` predicate, `achievedAppendL` / `achievedAppendR` list-append preservation, `LevelAchieved n cert` lifted to certificates, `composeAchievedL` / `composeAchievedR` proving any level achieved in either component of `composeCertificates` is still achieved in the composition. |
+| Proofs.idr | 0 | 0 | 0 | In package.  Attestation API hardened A7 (2026-04-18): every L1-L10 attestation now requires a witness from its level module (Schema / FieldIn / WasmTypeCompat / Ptr-NonNull / InBounds / AccessResult / ExclusiveWitness / EffectSubsumes / Lifetime.Outlives / CompletedProtocol).  `simpleReadCert` / `fullCert12` / `fullCert15` thread witnesses per level; the certificate cannot be constructed without real proof artefacts.  Level-achievement layer added A8 (2026-04-18): `LevelAchievedIn` predicate, `achievedAppendL` / `achievedAppendR` list-append preservation, `LevelAchieved n cert` lifted to certificates, `composeAchievedL` / `composeAchievedR` proving any level achieved in either component of `composeCertificates` is still achieved in the composition.  Attestation soundness A9 (2026-05-18): per-level `attestLN_Sound` family proving `LevelAchievedIn N [attestLN_X w]` — the weak "certificate claims level N" face.  **Witness-indexed redesign 2026-05-27 (PR #80, closes standards#130 long-tail)**: `LevelAttestationW : (n : Nat) -> Type` GADT with one ctor per level packaging the actual witness; 15 `attestLNW_*` smart ctors; 15 `attestLNW_Entails<Property>` extractors (the "attestation entails the level's semantic property" lemmas — a consumer holding `LevelAttestationW 7` can now discharge L7 alias-freeness via `ExclusiveWitness s`, not just the weak claim-predicate); `toLegacy` bridge; 15 round-trip `Refl`s; uniform `attestLW_AchievedIn` subsuming the A9 family.  **`WitnessCertificate` lift 2026-05-27 (PR #80, folded from #83)**: existential `SomeAttestationW` wrapper, `record WitnessCertificate` mirror of `ProofCertificate` with witness-carrying levels, `witnessToLegacy` bridge, `composeWitness` mirror, `composeWitnessLegacyAgree` compat lemma, `WitnessAchieved` predicate. |
 | Tropical.idr | 0 | 0 | 0 | In package (A1, 2026-04-18) |
 | Epistemic.idr | 0 | 0 | 0 | In package (A1, 2026-04-18) |
 | Echo.idr | 0 | 0 | 0 | In package (A0, 2026-04-18) |
+| VerifierSpec.idr | 0 | 0 | 0 | In package (2026-05-27, PR #79).  Spec-of-record for the Rust post-codegen verifier and the source-side checker.  Defines `ModuleSummary` / `FunctionSummary` / `OwnershipIntent` (mirrors the `typedwasm.ownership` custom section), structural acceptance predicates `TokenFresh` / `IntentsLinearAcceptable` / `FunctionsAccepted`, three acceptance predicates `SpecAccepts` / `VerifierAccepts` / `SourceAccepts` (the latter two carry a `TrustedFixture` inline so the differential ctor still terminates in a structural witness), the two **agreement records `VerifierSpecAgreement` (item 7) and `SourceVerifierAgreement` (item 8)** with totally-proven bodies, the concrete inhabitants `verifierSpecAgreement` / `sourceVerifierAgreement` (the first total no-`believe_me` agreement values in the codebase), end-to-end composition lemmas `sourceImpliesSpec` / `specImpliesSource` and `*Concrete` specialisations, demo modules (empty / `allocFreeModule` / `allocFreeWithBorrowModule` / `fixtureCleanLinearConsumerModule` mirrored from cross_compat row 1), and four discrimination proofs (`notSpecAcceptsBadDoubleConsume`, `notVerifierAcceptsBadDoubleConsume` ruling out BOTH ctors, `notSourceAcceptsBadDoubleConsume` ruling out BOTH ctors, `notSpecAcceptsBadDoubleProduce`) showing L10 has teeth and the differential escape hatch cannot smuggle a bad module past the verifier. |
 
 ## Post-codegen verifier (Rust)
 
@@ -133,7 +134,23 @@ files remain the spec of record until the cross-compat suite at
 real affinescript-emitted fixtures (deferred work, "C5.1").
 
 **Coverage:** L7 (ExclBorrow) + L10 (Linear) only.
-L1-L6, L13-L16 enforcement on emitted wasm is future work.
+L1-L6, L13-L16 enforcement on emitted wasm is future work
+(in progress on PRs #76 / #77 — wire-format proposal + L2 codec
+pre-staging behind `cfg(feature = "unstable-l2")`).
+
+**Spec-of-record alignment (2026-05-27, PR #79).**  The
+`TypedWasm.ABI.VerifierSpec` Idris2 module now states the
+**verifier ↔ spec ↔ source** agreement as totally-proven
+inhabitants of two records (`VerifierSpecAgreement`,
+`SourceVerifierAgreement`).  Closes the multi-week residual flagged
+by PR #74 ("Items 7 + 8 stated as obligations" from PR #72).  The
+Rust verifier's accept-verdicts on differential-harness fixtures are
+modelled via `TrustedFixture m` values that package the structural
+witness inline — the trust-injection moment is `MkTrustedFixture`
+construction (single grep point for audit).  A drift between this
+module and the Rust verifier's behaviour now shows up as either a
+failing differential-harness fixture or as an absent
+`TrustedFixture` registration.
 
 **Consumers** (live as of 2026-05-15):
 
diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md
index 508ec81..c402da9 100644
--- a/PROOF-NEEDS.md
+++ b/PROOF-NEEDS.md
@@ -20,6 +20,74 @@ compile time" (true) and "here is a lemma proving it is forbidden"
 claims — a reviewer asking _"where is the theorem?"_ currently has no
 answer to point at.
 
+## RECONCILIATION 2026-05-27 (post-A10 items 7 + 8 bodies closed — read this FIRST)
+
+> **The two agreement records introduced by PR #72 / A13 are now
+> inhabited.**  `VerifierSpecAgreement` and `SourceVerifierAgreement`
+> have concrete inhabitants `verifierSpecAgreement` /
+> `sourceVerifierAgreement` with totally-proven bodies in every
+> direction.  This was the "multi-week residual" PR #74 explicitly
+> flagged.  Closed in PR #79.
+>
+> **Design choice that unblocked the bodies.**  The differential
+> constructor carries the structural witness it certifies, packaged
+> inline via an embedded `TrustedFixture m`:
+>
+>     data VerifierAccepts : ModuleSummary -> Type where
+>       VAStructural   : FunctionsAccepted m.functions
+>                     -> VerifierAccepts m
+>       VADifferential : (fixture : TrustedFixture m)
+>                     -> VerifierAccepts m
+>
+>     record TrustedFixture (m : ModuleSummary) where
+>       constructor MkTrustedFixture
+>       trustedFixtureName : String
+>       trustedFixtureId   : Nat
+>       trustedWitness     : FunctionsAccepted m.functions
+>
+> Trust-injection moves to `MkTrustedFixture` construction (single
+> grep point for audit).  All four agreement lemmas become total by
+> case analysis: both `VAStructural` and `VADifferential` surface a
+> `FunctionsAccepted m.functions` payload that wraps directly into
+> `SpecAccepts`; the spec-to-verifier direction lifts via
+> `VAStructural`; source ↔ verifier mirror the same pattern.
+>
+> **Module: `src/abi/TypedWasm/ABI/VerifierSpec.idr` (~620 LOC).**
+> Zero `believe_me` / `assert_total` / `postulate` / `sorry` /
+> `assert_smaller`; `%default total`.  Build green 22/22 modules
+> under Idris2 0.8.0.  +33 Layer 1 regression assertions.
+>
+> **End-to-end demo.**  `fixtureCleanLinearConsumerModule` mirrors
+> cross_compat row 1.  `fixtureCleanLinearConsumerDifferentialAccepts`
+> exercises the smart constructor;
+> `fixtureCleanLinearConsumerSpecAccepts` runs the witness through
+> `verifierSpecAgreement.verifierIsSound` for the end-to-end
+> closure.
+>
+> **Discrimination.**  `notSpecAcceptsBadDoubleConsume`,
+> `notVerifierAcceptsBadDoubleConsume` (both ctors),
+> `notSourceAcceptsBadDoubleConsume` (both ctors),
+> `notSpecAcceptsBadDoubleProduce` — show L10 has teeth and the
+> differential escape hatch cannot smuggle a bad module past the
+> verifier (since `MkTrustedFixture` requires a structural witness,
+> which is impossible for the bad module).
+>
+> **Comparison with PR #74 (closed as superseded).**  #74 kept
+> `VADifferential` opaque (string + nat only) and offered
+> `Maybe`-returning bridges plus a closed-world `RegisteredFixture`
+> GADT.  Soundness/completeness for the unparameterised agreement
+> records remained unprovable in that design — that's the
+> "multi-week residual" #74's description named.  #79 refactors
+> the data type instead.  The audit story is preserved; the agreement
+> records cease to be obligations.
+>
+> **Open after this closure.**  Items remaining in the long-tail (in
+> rough decreasing priority): verifier L1-L6 + L13-L16 coverage on
+> emitted wasm (#34, #35; in progress on PRs #76 / #77 in a parallel
+> session), WasmCert-Isabelle tie-back, emitted-wasm byte-equality
+> (P3.1(a), blocked on emitter), parser round-trip in Idris2
+> (blocked on parser port).
+
 ## RECONCILIATION 2026-05-27 (standards#130 long-tail closed — read this FIRST)
 
 > **The "LevelAttestation reindexed by witness" residual is closed.**
diff --git a/README.adoc b/README.adoc
index 3f4c76e..7bee9df 100644
--- a/README.adoc
+++ b/README.adoc
@@ -109,6 +109,19 @@ Idris2 0.8.0 as of 2026-04-18 (see `PROOF-NEEDS.md` reconciliation). Their
 surface semantics remain research-grade — the parser, Zig FFI and downstream
 tooling do not yet expose L11/L12 features.
 
+[NOTE]
+.Spec-of-record for the Rust verifier (2026-05-27, PR #79)
+====
+`TypedWasm.ABI.VerifierSpec` is the Idris2 spec-of-record for
+`crates/typed-wasm-verify/`.  It carries totally-proven
+`VerifierSpecAgreement` and `SourceVerifierAgreement` records (with
+concrete inhabitants `verifierSpecAgreement` /
+`sourceVerifierAgreement`) bridging the spec to the verifier and the
+source checker — closes post-A10 audit items 7 + 8.  See the
+link:docs/wiki/Proof-Debt-Status.md[Proof-Debt-Status wiki page] for
+the design and what remains in the proof-debt long-tail.
+====
+
 == The Killer Feature: Multi-Module Type Safety
 
 When Module A (compiled from Rust) shares memory with Module B (compiled from
diff --git a/TEST-NEEDS.md b/TEST-NEEDS.md
index 50aa9fd..7746170 100644
--- a/TEST-NEEDS.md
+++ b/TEST-NEEDS.md
@@ -6,14 +6,14 @@
 
 | Category | Count | Details |
 |----------|-------|---------|
-| **Source modules** | 21 | 11 Idris2 ABI (Region, TypedAccess, Levels, Pointer, Effects, Lifetime, Linear, MultiModule, Proofs, Tropical, Epistemic), 4 AffineScript parser (Ast, Parser, Lexer, Checker), 3 Idris2 interface ABI, 2 Zig FFI + cache, 1 Rust verifier crate (typed-wasm-verify, ~1.6k LOC + 53 tests) |
+| **Source modules** | 22 | 12 Idris2 ABI (Region, TypedAccess, Levels, Pointer, Effects, Lifetime, Linear, MultiModule, Proofs, Tropical, Epistemic, **VerifierSpec — added 2026-05-27 via PR #79** as the spec-of-record for the Rust post-codegen verifier), 4 AffineScript parser (Ast, Parser, Lexer, Checker), 3 Idris2 interface ABI, 2 Zig FFI + cache, 1 Rust verifier crate (typed-wasm-verify, ~1.6k LOC + 53 tests) |
 | **Unit tests** | 2 files | ParserTests.affine (88 assertions), crates/typed-wasm-verify (43 unit + 10 cross-compat) |
 | **Integration tests** | 1 | tests/contracts/airborne-step-state-contract.mjs (14 assertions) |
 | **E2E tests** | 2 | tests/smoke/e2e-smoke.mjs (40 assertions), tests/e2e/e2e-driver.mjs (corpus driver) |
 | **Per-level tests** | 10 | tests/levels/L1.mjs .. L10.mjs (56 assertions total) |
-| **Aspect tests** | 2 | tests/aspect/claim-envelope.mjs (49 assertions — added 2026-05 to catch cross-doc claim drift after deep audit found 5 such drifts), tests/aspect/security-envelope.mjs (10 assertions — added 2026-05-24 to catch SECURITY.md/security.txt drift, SPDX gaps, badge-vs-reality, committed secrets) |
-| **Property-based tests** | 1 | tests/property/property_test.mjs (29 assertions across 6 invariants P1-P6: parser determinism, comment stability, diagnostic positional consistency, example-corpus liveness, level-fixture coverage, 5-trial stability — added 2026-05-24, closes the 2026-04-04 ghost) |
-| **Proof regression** | 1 | tests/proof/regression.mjs (25 named-theorem presence assertions + optional idris2 --check layer — added 2026-05-24) |
+| **Aspect tests** | 2 | tests/aspect/claim-envelope.mjs (53 assertions — added 2026-05, bumped 49→53 in PR #60 for §8 drift detection), tests/aspect/security-envelope.mjs (10 assertions — added 2026-05-24) |
+| **Property-based tests** | 1 | tests/property/property_test.mjs (29 assertions across 6 invariants P1-P6) |
+| **Proof regression** | 1 | tests/proof/regression.mjs (107 named-theorem presence assertions + optional idris2 `--build` layer; bumped 25→58→107 across 2026-05-24, PR #79 +33, PR #80 +49) |
 | **Benchmarks** | 1 | benchmarks/parser-bench.mjs (per-example wallclock; median/p95/min/throughput; JSON summary on stderr; added 2026-05) |
 | **ECHIDNA harness** | 1 | tests/echidna/echidna-harness.mjs (659 LOC, 124 local assertions, remote prover-wars submission) |
 
diff --git a/docs/supplementary/proof-inventory.adoc b/docs/supplementary/proof-inventory.adoc
index 74db817..1a816a9 100644
--- a/docs/supplementary/proof-inventory.adoc
+++ b/docs/supplementary/proof-inventory.adoc
@@ -102,6 +102,73 @@ root.  Every file is compiled with `%default total`; no `believe_me`,
 |Status |✓ Type-checked; compatibility is a compile-time obligation
 |===
 
+[[thm-verifier-spec-agreement]]
+=== Theorem: Verifier ↔ Spec Agreement (§Post-Codegen Verifier) — added 2026-05-27
+
+[cols="1,3"]
+|===
+|Claim |The Rust post-codegen verifier (`crates/typed-wasm-verify/`)
+        accepts a module if and only if the Idris2 spec (`SpecAccepts`)
+        does — `verifierIsSound` (verifier accept ⇒ spec accept) and
+        `verifierIsComplete` (spec accept ⇒ verifier accept), bundled
+        in a `VerifierSpecAgreement` record.  Symmetric
+        `SourceVerifierAgreement` for source-checker ↔ verifier.
+|File |`VerifierSpec.idr` (added in PR #79)
+|Type |`record VerifierSpecAgreement` + `record SourceVerifierAgreement`,
+       each bundling soundness and completeness as named fields.
+|Construction |`verifierSpecAgreement : VerifierSpecAgreement` and
+               `sourceVerifierAgreement : SourceVerifierAgreement` —
+               concrete inhabitants, the first total no-`believe_me`
+               agreement values in the codebase.  Built from the four
+               total lemmas `verifierIsSound`, `verifierIsComplete`,
+               `sourceImpliesVerifier`, `verifierImpliesSource`.
+|Design |The differential constructor `VADifferential` carries an
+         inline `TrustedFixture m` (fixture name + id + structural
+         witness).  Trust-injection moves to `MkTrustedFixture`
+         construction (single grep point for audit), and all four
+         agreement directions become total by case analysis.
+|Coverage |Spec surface = L7 (aliasing) + L10 (linearity) — same as the
+           Rust verifier's current coverage.  Extending to L1-L6 +
+           L13-L16 is tracked under issues #34 / #35 and PRs #76 / #77.
+|Status |✓ Fully proven at the spec-of-record level for the current
+         verifier coverage envelope
+|===
+
+[[thm-attestation-entails-semantic-property]]
+=== Theorem: Attestation Entails the Level's Semantic Property — added 2026-05-27
+
+[cols="1,3"]
+|===
+|Claim |Holding a level-N attestation entails recovery of the level-N
+        semantic-property witness (closes the standards#130 long-tail
+        item the 2026-05-18 PROOF-NEEDS reconciliation flagged).
+|File |`Proofs.idr` (extended in PR #80)
+|Type |`data LevelAttestationW : (n : Nat) -> Type` — witness-indexed
+       attestation GADT, one constructor per level (L1-L15).  Each
+       packages the level-specific witness (`Schema`, `FieldIn`,
+       `WasmTypeCompat`, …, `FunctionCaps`).
+|Extractors |15 per-level `attestLNW_Entails<Property>` lemmas (total
+             pattern-match functions returning the witness, paired
+             with its existential type-level indices where applicable).
+             E.g. `attestL7W_EntailsAliasFree : LevelAttestationW 7 ->
+             (s : Schema ** ExclusiveWitness s)`.
+|Legacy bridge |`toLegacy : {n : Nat} -> LevelAttestationW n ->
+                LevelAttestation` projects to the unindexed shape so
+                existing callers of `List LevelAttestation` (e.g.
+                `ProofCertificate`) keep working unchanged.  15 round-
+                trip `Refl` equalities pin the witness-carrying and
+                legacy representations together.
+|Certificate lift |`record WitnessCertificate` (mirror of
+                   `ProofCertificate`) carries `List SomeAttestationW`
+                   (existential wrapper hiding the level index).
+                   `witnessToLegacy` projects down; `composeWitness`
+                   mirrors `composeCertificates`;
+                   `composeWitnessLegacyAgree` is the composition
+                   compatibility lemma.
+|Status |✓ Fully proven; purely additive (no existing definition
+         modified, no prior proof regresses)
+|===
+
 == Level-to-File Mapping
 
 [cols="1,2,2,1"]
diff --git a/docs/wiki/Home.md b/docs/wiki/Home.md
index 6dd1af6..7e5da89 100644
--- a/docs/wiki/Home.md
+++ b/docs/wiki/Home.md
@@ -4,7 +4,7 @@
 
 ## Status
 
-Pre-alpha / research. Foundation defensibly engineered as of 2026-05-24. See [Phase-0-Status](Phase-0-Status) for what's done and what remains.
+Pre-alpha / research. Foundation defensibly engineered as of 2026-05-24; proof-debt long-tail items closed in a 2026-05-27 sweep. See [Phase-0-Status](Phase-0-Status) for the engineering surface, and [Proof-Debt-Status](Proof-Debt-Status) for what's mechanically proven, what's outstanding, and what's blocked.
 
 The path from here to a production-quality compile target adopted outside the hyperpolymath ecosystem is laid out as a 6-phase plan in [Production-Path](Production-Path) and [`docs/PRODUCTION-PATH.adoc`](https://github.com/hyperpolymath/typed-wasm/blob/main/docs/PRODUCTION-PATH.adoc). See [Comparison](Comparison) for how typed-wasm sits among neighbouring approaches at each maturity level.
 
@@ -50,7 +50,7 @@ Levels are progressive — you cannot skip from L1 to L7. L11 (tropical cost-tra
 
 Follows the hyperpolymath ABI-FFI standard:
 
-- **Idris2 ABI** (`src/abi/TypedWasm/ABI/`) — formal dependent-type proofs; 0 `believe_me`, 0 `assert_total`, 0 `postulate`
+- **Idris2 ABI** (`src/abi/TypedWasm/ABI/`) — formal dependent-type proofs; 0 `believe_me`, 0 `assert_total`, 0 `postulate`. Includes `TypedWasm.ABI.VerifierSpec` (added 2026-05-27 via PR #79) as the Idris2 spec-of-record for the Rust post-codegen verifier — with totally-proven `VerifierSpecAgreement` / `SourceVerifierAgreement` records bridging the spec to verifier and source-checker. See [Proof-Debt-Status](Proof-Debt-Status) for the inventory.
 - **Zig FFI** (`ffi/zig/`) — C-ABI bridge for runtime region management + typed load/store
 - **Rust verifier** (`crates/typed-wasm-verify/`) — post-codegen verification of the 10-level discipline against compiled wasm
 - **Surface syntax** (`spec/grammar.ebnf`) — `.twasm` source format (EBNF)
diff --git a/docs/wiki/Phase-0-Status.md b/docs/wiki/Phase-0-Status.md
index 34b48fb..36a82b3 100644
--- a/docs/wiki/Phase-0-Status.md
+++ b/docs/wiki/Phase-0-Status.md
@@ -110,3 +110,18 @@ None of D1–D6 from [Production-Path](Production-Path) have ADRs yet. D2 (produ
 ## What unblocks Phase 1
 
 Track A's codegen v0 PR. Track B can land in parallel without blocking the gate.
+
+## 2026-05-27 — Post-Phase-0 proof-debt closure pass
+
+Independent of the Phase 0 / Phase 1 gate transition, a 2026-05-27 sweep closed long-tail proof-debt items the 2026-05-18 PROOF-NEEDS reconciliation banner had deferred. See the dedicated [Proof-Debt-Status](Proof-Debt-Status) page for the full inventory.
+
+| PR | What it lands | Closes |
+|---|---|---|
+| [#79](https://github.com/hyperpolymath/typed-wasm/pull/79) | `TypedWasm.ABI.VerifierSpec` — total bodies for `VerifierSpecAgreement` + `SourceVerifierAgreement` | Post-A10 audit items 7 + 8 |
+| [#80](https://github.com/hyperpolymath/typed-wasm/pull/80) | `LevelAttestationW` witness-indexed GADT + `WitnessCertificate` heterogeneous-list lift | standards#130 "attestation entails the level's semantic property" long-tail |
+| [#74](https://github.com/hyperpolymath/typed-wasm/pull/74) | Closed as superseded by #79 (Maybe-bridge design replaced by witness-carrying ctor design) | — |
+
+**Test surface 545 → 627+ assertions** (proof regression 25 → 107 from +33 #79 + +49 #80).
+**Zero new `believe_me` / `assert_total` / `postulate` / `sorry` / `assert_smaller`; `%default total` preserved.**
+
+These PRs are independent of the Phase 0 → Phase 1 gate (which is still blocked on codegen v0). They close debt items that would otherwise haunt the v1.0 audit.
diff --git a/docs/wiki/Proof-Debt-Status.md b/docs/wiki/Proof-Debt-Status.md
new file mode 100644
index 0000000..472546b
--- /dev/null
+++ b/docs/wiki/Proof-Debt-Status.md
@@ -0,0 +1,187 @@
+# Proof Debt Status
+
+**What's mechanically proven in typed-wasm, what's outstanding, and what's blocked on prerequisites.**
+
+This page is for readers asking _"where is the theorem?"_ when faced with typed-wasm's safety claims. The proofs live in `src/abi/TypedWasm/ABI/*.idr` and are mechanically checked by Idris2 0.8.0. The detailed inventory lives in [`PROOF-NEEDS.md`](https://github.com/hyperpolymath/typed-wasm/blob/main/PROOF-NEEDS.md) and [`LEVEL-STATUS.md`](https://github.com/hyperpolymath/typed-wasm/blob/main/LEVEL-STATUS.md); this page summarises and links.
+
+## Invariants
+
+- **0 `believe_me`** in the checked package
+- **0 `assert_total`** in the checked package
+- **0 `postulate`** in the checked package
+- **0 `sorry`** / **0 `Admitted`** in the checked package
+- **0 `assert_smaller`** in the checked package
+- **`%default total`** everywhere
+
+Verified by `tests/proof/regression.mjs` (107 named-theorem grep assertions) and by `idris2 --build src/abi/typed-wasm.ipkg` (22/22 modules under Idris2 0.8.0).
+
+## The proof package
+
+22 Idris2 modules. Per-module status is in `LEVEL-STATUS.md` §"Proof inventory"; the headline:
+
+| Module | Role |
+|---|---|
+| `Region.idr` | Schema + FieldIn (L1, L2, L5 structural primitives) |
+| `TypedAccess.idr` | Typed load/store + AccessResult (L3, L6) |
+| `Levels.idr` | Canonical L1-L10 data types |
+| `Pointer.idr` | Pointer kinds + ExclusiveWitness (L4, L7) |
+| `Effects.idr` | Effect-set + subsumption (L8) |
+| `Lifetime.idr` | Outlives preorder + load-safety (L9) |
+| `Linear.idr` | CompletedProtocol + linear discipline (L10) |
+| `MultiModule.idr` | Schema-subtype + no-spoofing theorem (cross-module) |
+| `Tropical.idr` | Cost-bounded paths (L11, draft) |
+| `Epistemic.idr` | Freshness propagation (L12, draft) |
+| `ModuleIsolation.idr` | Per-module memory isolation (L13) |
+| `SessionProtocol.idr` | Session protocols + WellFormedProtocol (L14) |
+| `ResourceCapabilities.idr` | Capability lattice (L15) |
+| `Choreography.idr` | Composition over L13+L14+L15 (L16) |
+| `Layout.idr` + `Layout/*.idr` | Cross-language layout contracts |
+| `Echo.idr` | Echo composition (research) |
+| `Proofs.idr` | Top-level certificate assembly + witness-indexed attestation API + WitnessCertificate lift |
+| **`VerifierSpec.idr`** | **Spec-of-record for the Rust post-codegen verifier (added 2026-05-27 via PR #79)** |
+
+## Recently closed (2026-05-27 sweep)
+
+The 2026-05-18 PROOF-NEEDS reconciliation banner deferred several long-tail items. A 2026-05-27 sweep closed three of them:
+
+### Item 7 + Item 8 — Verifier ↔ spec ↔ source agreement (PR #79)
+
+The post-A10 audit (item 7: Rust verifier ↔ Idris2 spec equivalence; item 8: source-checker ↔ verifier coverage agreement) stated two record obligations:
+
+```idris
+record VerifierSpecAgreement where
+  constructor MkVerifierSpecAgreement
+  verifierIsSound    : (m : ModuleSummary) -> VerifierAccepts m -> SpecAccepts m
+  verifierIsComplete : (m : ModuleSummary) -> SpecAccepts m -> VerifierAccepts m
+
+record SourceVerifierAgreement where
+  constructor MkSourceVerifierAgreement
+  sourceImpliesVerifier : (m : ModuleSummary) -> SourceAccepts m -> VerifierAccepts m
+  verifierImpliesSource : (m : ModuleSummary) -> VerifierAccepts m -> SourceAccepts m
+```
+
+PR #74 attempted these with `Maybe`-returning bridges and a closed-world `RegisteredFixture` GADT, but the records themselves remained uninhabited — #74 explicitly called this "the multi-week residual".
+
+**PR #79 closes the bodies** by refactoring the differential constructor to carry the structural witness inline:
+
+```idris
+data VerifierAccepts : ModuleSummary -> Type where
+  VAStructural   : FunctionsAccepted m.functions -> VerifierAccepts m
+  VADifferential : (fixture : TrustedFixture m)  -> VerifierAccepts m
+
+record TrustedFixture (m : ModuleSummary) where
+  constructor MkTrustedFixture
+  trustedFixtureName : String
+  trustedFixtureId   : Nat
+  trustedWitness     : FunctionsAccepted m.functions
+```
+
+The trust-injection moment moves to `MkTrustedFixture` construction (single grep point for audit). All four agreement lemmas become total by case analysis. `verifierSpecAgreement : VerifierSpecAgreement` and `sourceVerifierAgreement : SourceVerifierAgreement` are concrete inhabitants — the first total no-`believe_me` agreement values in the codebase.
+
+End-to-end demo on cross_compat row 1 (`fixtureCleanLinearConsumerModule`). Four discrimination proofs show L10 has teeth and the differential escape hatch cannot smuggle a bad module past the verifier.
+
+### standards#130 — LevelAttestation reindexed-by-witness (PR #80)
+
+The 2026-05-18 banner flagged:
+
+> "Stronger 'attestation entails the level's semantic property' (needs `LevelAttestation` reindexed by witness) remains tracked future work under standards#130."
+
+The A9 work proved `LevelAchievedIn N [attestLN_X w]` — i.e. "the certificate provably claims level N". But that's the weaker face: anyone holding the attestation cannot recover the underlying witness (`ExclusiveWitness s` for L7, etc.) because the legacy `attestLN_*` family discards it.
+
+**PR #80 closes this** with a witness-indexed GADT:
+
+```idris
+data LevelAttestationW : (n : Nat) -> Type where
+  AttestL7W : {s : Schema} -> (w : ExclusiveWitness s) -> LevelAttestationW 7
+  -- … 14 more constructors, one per level
+
+attestL7W_EntailsAliasFree :
+     LevelAttestationW 7
+  -> (s : Schema ** ExclusiveWitness s)
+attestL7W_EntailsAliasFree (AttestL7W {s} w) = (s ** w)
+```
+
+A consumer holding `LevelAttestationW 7` can now discharge the L7 semantic property (alias-freeness via `ExclusiveWitness s`) — not just the weak claim-predicate. Purely additive: legacy `LevelAttestation`, `MkAttestation`, `attestLN_*`, `attestLN_Sound`, `LevelAchievedIn`, `composeCertificates`, `ProofCertificate` are all unchanged. 15 ctors + 15 smart ctors + 15 extractors + legacy bridge + 15 round-trip `Refl`s + uniform `attestLW_AchievedIn` (subsuming the A9 family).
+
+### WitnessCertificate — heterogeneous-list lift (PR #80, folded from #83)
+
+`LevelAttestationW n` retains the witness per attestation, but `ProofCertificate` still uses `List LevelAttestation` for its `levels` field, so a heterogeneous certificate can't be built directly. **PR #83 (folded into #80)** adds an existential wrapper:
+
+```idris
+data SomeAttestationW : Type where
+  MkSomeAttW : {n : Nat} -> (att : LevelAttestationW n) -> SomeAttestationW
+
+record WitnessCertificate where
+  constructor MkWitnessCert
+  witnessLevels        : List SomeAttestationW
+  witnessHighestProven : Nat
+  witnessMultiModule   : List CompatCertificate
+
+witnessToLegacy : WitnessCertificate -> ProofCertificate
+composeWitness  : WitnessCertificate -> WitnessCertificate -> WitnessCertificate
+WitnessAchieved : (n : Nat) -> WitnessCertificate -> Type
+```
+
+The `composeWitnessLegacyAgree` lemma pins down: composing the legacy projections equals projecting the witness composition — the two paths stay consistent.
+
+## Outstanding long-tail items
+
+In rough decreasing priority:
+
+### Verifier L1–L6 + L13–L16 coverage on emitted wasm (#34 / #35)
+
+**Status:** in progress on PRs #76 (carrier-section wire-format proposal) + #77 (L2 codec pre-staged behind `cfg(feature = "unstable-l2")`). DO NOT interfere — actively worked by a parallel session.
+
+The Rust verifier currently covers L7 (aliasing) + L10 (linearity) only. Extending it requires a multi-producer ABI change: a new custom section for L2-L6 region/field schema + nullability + cardinality, and another for the L15 capability lattice. Coordinated across `hyperpolymath/{typed-wasm,ephapax,affinescript}`.
+
+### WasmCert-Isabelle tie-back
+
+**Status:** not started. Tracked in `docs/supplementary/proof-inventory.adoc:45`, `docs/WHITEPAPER.md:602`, `LEVEL-STATUS.md:66`. Requires external Isabelle/HOL artifact + bridge; multi-week. The goal is to connect typed-wasm's `Region.idr` semantics to the WasmCert mechanised operational semantics so the L1-L6 claims can be discharged against a reference wasm semantics, not just paper-equivalents.
+
+### Emitted-wasm byte-equality (P3.1(a))
+
+**Status:** blocked on emitter. PROOF-NEEDS.md:442 explicitly says: "blocked pending a `.twasm`→`.wasm` emitter". Once an emitter lands, extend `tests/echidna/echidna-harness.mjs` Property 5 to run both sides through the emitter and `assertBytesEqual`.
+
+### Parser round-trip in Idris2
+
+**Status:** blocked on parser port. The AffineScript parser is OCaml (`lib/ocaml/Parser.affine`). The ECHIDNA-side fuzz property is doable today; the Idris2 mechanical proof is blocked on the Track A AffineScript→Idris2 parser port.
+
+## How the proofs relate to runtime safety
+
+| Layer | What it proves | Where |
+|---|---|---|
+| **Idris2 proofs** | Type discipline is sound (spec-level): every well-typed program respects L1-L10 / L13-L16 | `src/abi/TypedWasm/ABI/*.idr` |
+| **Source checker** | Source programs respect the discipline | `hyperpolymath/affinescript:lib/codegen.ml` (QTT pass), upcoming `.twasm` parser/checker |
+| **Post-codegen verifier** | Emitted wasm bytes respect the discipline (covers L7 + L10 today) | `crates/typed-wasm-verify/` (Rust) + `hyperpolymath/affinescript:lib/{tw_verify,tw_interface}.ml` (OCaml, reference impl) |
+| **Spec-of-record (2026-05-27)** | Verifier and source-checker agree with the Idris2 spec — bundled as totally-proven records | `src/abi/TypedWasm/ABI/VerifierSpec.idr` (NEW) |
+
+The agreement records introduced in PR #79 close the loop: a drift between the Rust verifier's accept-verdict on a fixture and the Idris2 spec's `SpecAccepts` predicate now shows up either as a failing differential-harness fixture or as an absent `TrustedFixture` registration. Trust is injected once per audited fixture, not at every consumer.
+
+## Build and test oracle
+
+```bash
+# Build the proof package
+IDRIS2_PREFIX=$IDRIS2/0.8.0 idris2 --build src/abi/typed-wasm.ipkg
+# expects: 22/22 modules, rc=0
+
+# Run the proof regression
+PATH=$IDRIS2/0.8.0/bin:$PATH \
+IDRIS2_PREFIX=$IDRIS2/0.8.0 \
+  node tests/proof/regression.mjs --strict
+# expects: 107 passed, 0 failed, 0 skipped
+
+# Verify no banned patterns
+grep -rnE "believe_me|assert_total|postulate|sorry|Admitted|assert_smaller" \
+  src/abi/TypedWasm/ABI/*.idr \
+  | grep -vE "^[^:]+:[0-9]+:--|^[^:]+:[0-9]+:[[:space:]]*--|^[^:]+:[0-9]+:\|\|\|"
+# expects: no output (only banner comments mention banned patterns)
+```
+
+## See also
+
+- [`PROOF-NEEDS.md`](https://github.com/hyperpolymath/typed-wasm/blob/main/PROOF-NEEDS.md) — full per-obligation inventory with reconciliation banners
+- [`LEVEL-STATUS.md`](https://github.com/hyperpolymath/typed-wasm/blob/main/LEVEL-STATUS.md) — per-module believe_me / postulate / assert_total status + post-codegen verifier coverage
+- [`docs/supplementary/proof-inventory.adoc`](https://github.com/hyperpolymath/typed-wasm/blob/main/docs/supplementary/proof-inventory.adoc) — paper-facing summary
+- [`CHANGELOG.md`](https://github.com/hyperpolymath/typed-wasm/blob/main/CHANGELOG.md) — dated PR landings
+- [Phase-0-Status](Phase-0-Status) — Phase 0 engineering surface (orthogonal to proof debt)
+- [Production-Path](Production-Path) — the 6-phase plan
diff --git a/docs/wiki/README.md b/docs/wiki/README.md
index e124a85..78b01e5 100644
--- a/docs/wiki/README.md
+++ b/docs/wiki/README.md
@@ -30,7 +30,8 @@ git push
 |---|---|
 | `Home.md` | Wiki landing page; current state + links to other pages |
 | `Production-Path.md` | The 6-phase production plan (companion to `docs/PRODUCTION-PATH.adoc`) |
-| `Phase-0-Status.md` | Live closure state with PR cross-links + test surface summary |
+| `Phase-0-Status.md` | Live closure state with PR cross-links + test surface summary; plus a 2026-05-27 post-Phase-0 proof-debt closure section |
+| `Proof-Debt-Status.md` | What's mechanically proven, what's outstanding, what's blocked on prerequisites; the page to point at when asked "where is the theorem?" (added 2026-05-27) |
 | `Comparison.md` | Landscape of typed-wasm vs neighbouring approaches at each maturity level |
 
 ## Authoring rules