diff --git a/README.md b/README.md
index 0c571ec..92dbb16 100644
--- a/README.md
+++ b/README.md
@@ -8,9 +8,10 @@ four ed25519 campaigns (`dalek/anza/risc0/betrusted-ed25519-verified`).
 ## STATUS: eleven certificates over the extracted verify model (external review rounds 1–6 applied)
 
 `verification/check.sh` is **green** (exit 0): the model compiles, the proofs
-compile, and the audit passes. The audit runs **inside Lean**
-(`verification/Proofs/Audit.lean`) and binds four things, each added because an
-external reviewer *demonstrated* the button going green without it:
+compile, and the audit passes. It binds **six** things, each added because an
+external reviewer *demonstrated* the button going green without it. Four are
+checked **inside Lean** by `verification/Proofs/Audit.lean`; the last two are
+separate phases that deliberately do **not** rely on that file:
 
 - **axiom cones** — each certificate's cone is read from the kernel via
   `collectAxioms` and must equal its expected set EXACTLY, so an added axiom
@@ -26,9 +27,26 @@ external reviewer *demonstrated* the button going green without it:
   *body*. Round 5 showed why the last part is essential: redefining a fold to
   *be* the extracted loop left every earlier fingerprint bit-identical while the
   certificate degenerated to "the loop equals the loop";
-- **bytes** — Phase 0 sha256-pins the four model files and the compiler harness
+- **bytes** — Phase 0 sha256-pins the five model files and the compiler harness
   `lean-guard`, purges stale `.olean`s, and forbids stray `.lean` files, so the
-  verdict depends on committed bytes rather than build-directory state.
+  verdict depends on committed bytes rather than build-directory state;
+- **correspondence** (Phase 0d) — byte pins say the model did not *change*; they
+  say nothing about whether it *answers the extraction*. Aeneas states what the
+  extracted Rust needs from outside in `FunsExternal_Template.lean`, and every
+  such name must be answered by the hand-written model or by a real definition
+  in the corpus. An **extra axiom** in the model — an assumption no template
+  asks for — fails the button rather than passing as a silent row. This
+  repository previously deleted the template on every run, which is exactly why
+  it shipped a Template/model pair with no correspondence check at all
+  (round-8 estate review, GPT-5.6);
+- **the object files** (Phase 3b) — a second, independently implemented axiom
+  gate that reads the compiled `.olean`s via `readModuleData` instead of the
+  elaboration-time environment. Phase 3's view has a demonstrated blind spot: a
+  declaration made *after* the command that performs the walk sits in the object
+  file but not in the environment while the walk runs, so the walker reports "no
+  axiom" and is telling the truth about what it could see. Verified here by
+  planting `axiom cheat : ∀ (P : Prop), P` after the audit command — Phase 3
+  passed it, Phase 3b rejected it.
 
 What the button still does **not** bind is stated plainly in
 [TRUSTED-BASE.md](TRUSTED-BASE.md) item 11 — `check.sh` itself, the toolchain
diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md
index 7cdee30..9fa7c49 100644
--- a/TRUSTED-BASE.md
+++ b/TRUSTED-BASE.md
@@ -20,6 +20,27 @@ proceeds and is part of every claim.
    toolchain) are trusted to preserve semantics from Rust (MIR) to the
    Lean model. Divergence between rustc's semantics and the extracted
    model is trusted base.
+
+   **What is now reproducible, and what is not.** Extraction is two steps:
+   `Rust --charon--> SlhVerify.llbc --aeneas--> gen/SlhVerify/*.lean`. The
+   `.llbc` is committed, so the SECOND step can be re-run by anyone with the
+   pinned Aeneas and this repository, and on 2026-08-03 doing so reproduced
+   `Types.lean` and `Funs.lean` **byte-identically**. The FIRST step still
+   requires charon, which no reviewer has yet had available. So: the
+   LLBC → Lean half is reproducible on demand; the Rust → LLBC half rests on
+   the author's attestation alone, and continues to do so until a third party
+   runs it. Do not read the first half as evidence for the second.
+
+3b. **The correspondence check is textual, not a Lean query.** Phase 0d parses
+   `FunsExternal_Template.lean` and the hand-written model as SOURCE TEXT. It
+   establishes that every external the extraction names is answered by a
+   declaration of the right name in the pinned model, and that the model
+   declares no axiom the extraction never asked for. It does **not** ask Lean
+   how those names resolve at elaboration — the four ed25519 repositories have
+   a second, semantic phase for that; this one does not. All eleven externals
+   here are answered by the model itself (none by the proven corpus), which is
+   the narrow case where the textual answer and the semantic one coincide, but
+   that is a property of today's corpus and not a guarantee of the check.
 4. **The Lean kernel and its three axioms**
    (`propext, Classical.choice, Quot.sound`).
 5. **Build correspondence.** No reproducible-builds claim: the proof is
diff --git a/verification/check.sh b/verification/check.sh
index 708f23e..1057974 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -7,6 +7,11 @@
 #             depend on committed bytes, not untracked build state), forbid any
 #             .lean outside gen/ and Proofs/, and sha256-pin the four model files
 #             AND the compiler harness `lean-guard` to PROVENANCE.json.
+#   Phase 0d— template/model correspondence: every external Aeneas states the
+#             extracted Rust needs (FunsExternal_Template.lean, committed and
+#             pinned) must be answered by the hand-written model or by a real
+#             definition in the corpus. An EXTRA AXIOM in the model — an
+#             assumption no template asks for — is a failure, not a silent row.
 #   Phase 1 — compile the extracted Lean model (gen/SlhVerify).
 #   Phase 2 — compile the proof files (Proofs/).
 #   Phase 3 — the in-Lean audit (Proofs/Audit.lean): per certificate, the cone
@@ -17,6 +22,14 @@
 #             POLICY constants, every certificate STATEMENT, and every reachable
 #             SPECIFICATION DEFINITION BODY. Any mismatch → non-zero exit →
 #             fail-closed. No text parsing of axiom cones.
+#   Phase 3b— kernel-side axiom-declaration gate: reads the compiled OBJECT
+#             FILES (`readModuleData`) rather than the elaboration-time
+#             environment, and rejects any axiom declared under Proofs/. This is
+#             a SECOND, independently implemented gate on the same property,
+#             because Phase 3's view has a demonstrated blind spot: a
+#             declaration made after the command that performs the walk is in
+#             the object file but not in the environment while the walk runs.
+#             It runs after Phase 3 because Proofs/Audit.lean is compiled there.
 #
 #   What this button does NOT bind is stated in TRUSTED-BASE.md item 11: this
 #   script itself, the toolchain env, $AENEAS_HOME, and the Lean toolchain.