diff --git a/.gitignore b/.gitignore
index 5df2ca2..c225d7d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,5 +1,7 @@
 *.olean
 target/
 .lake/
-*_Template.lean
+# *_Template.lean is NO LONGER ignored: it is Aeneas's own statement of what
+# the extraction needs from outside, and it is the only artifact against which
+# "does the model ANSWER the extraction" can be asked. Committed and pinned.
 SlhVerify.llbc
diff --git a/verification/MODEL-CORRESPONDENCE.txt b/verification/MODEL-CORRESPONDENCE.txt
new file mode 100644
index 0000000..99a9624
--- /dev/null
+++ b/verification/MODEL-CORRESPONDENCE.txt
@@ -0,0 +1,12 @@
+SlhVerify/FunsExternal|Array.Insts.ZeroizeZeroize.zeroize|MODEL
+SlhVerify/FunsExternal|U32.Insts.CoreIterRangeStep.backward_checked|MODEL
+SlhVerify/FunsExternal|U32.Insts.CoreIterRangeStep.forward_checked|MODEL
+SlhVerify/FunsExternal|U32.Insts.CoreIterRangeStep.steps_between|MODEL
+SlhVerify/FunsExternal|verify_mono.oracle.f|MODEL
+SlhVerify/FunsExternal|verify_mono.oracle.h|MODEL
+SlhVerify/FunsExternal|verify_mono.oracle.h_msg|MODEL
+SlhVerify/FunsExternal|verify_mono.oracle.t_l|MODEL
+SlhVerify/FunsExternal|verify_mono.oracle.t_len|MODEL
+SlhVerify/FunsExternal|zeroize.Zeroize.Blanket.zeroize|MODEL
+SlhVerify/FunsExternal|zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop|MODEL
+CORRESPONDENCE-COUNT|11
diff --git a/verification/PROVENANCE.json b/verification/PROVENANCE.json
index cdc7aca..a58bcb6 100644
--- a/verification/PROVENANCE.json
+++ b/verification/PROVENANCE.json
@@ -42,7 +42,8 @@
     "gen/SlhVerify/TypesExternal.lean": "2988c04c5fc8c634aff4d9bd13604b8a47e677daa1f45e8f4f321368606cdd0a",
     "gen/SlhVerify/FunsExternal.lean": "5efe551c35969c9da28b2f3eaed4a6a67c410c62a1926aab390e3abf010390f8",
     "gen/SlhVerify/Types.lean": "db720b4a30f512e6048212a472e6853b24931a8121cb94c4cf7e6489754d6384",
-    "gen/SlhVerify/Funs.lean": "7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f"
+    "gen/SlhVerify/Funs.lean": "7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f",
+    "gen/SlhVerify/FunsExternal_Template.lean": "b4f9c6ecdbd55599bc4d35720fff1accc71475b5702410b5a0666456439a4042"
   },
   "harness_integrity_sha256": {
     "_comment": "The harness is part of the trusted computing base and its membership is now SELF-DERIVING: check.sh requires every executable file in verification/ to appear here (round-8 review \u2014 a hardcoded list was itself a second thing to keep in sync), plus Proofs/Audit.lean, which is not executable but computes the digest it is judged by. check.sh itself is excluded: it cannot pin itself, and is disclosed as trusted-unbound in TRUSTED-BASE.md item 11. Pinning check-selftest.sh matters beyond the button: it is the only artifact demonstrating the gates work, and its assertions have been defective in four consecutive rounds, so weakening it is now a reviewable pin rotation rather than an unnoticed edit.",
@@ -50,7 +51,9 @@
     "Proofs/Audit.lean": "6108b97d75a8a8e8e0b9bef642ba887ea1ae8b17ba5b7c11d66400bfd2847d9e",
     "check-selftest.sh": "c6811482e25ae6e1fffa6ca50e60541e8e609a70c951db6bec4d2d39a4849e9a",
     "drill.sh": "915cf9310fa168c14ca5d76a1b84fd3b19acdfef9dfd0b03b01b19883548719e",
-    "extract.sh": "01cff43c350ed8eaac0e65ccd7599b68fef47c9434cdb5ad01c92d2127a3bbe9"
+    "extract.sh": "01cff43c350ed8eaac0e65ccd7599b68fef47c9434cdb5ad01c92d2127a3bbe9",
+    "model-correspondence.py": "1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427",
+    "MODEL-CORRESPONDENCE.txt": "77bd374a60152689edcb3350c2a2547c6aaad192629e39e86d8548d2bad3f748"
   },
   "audit_gate": "verification/Proofs/Audit.lean \u2014 in-Lean audit (round 5). Per certificate: exact cone equality (collectAxioms) + elaborated-statement check. Enumeration: EVERY declaration kind (def/theorem/opaque/axiom \u2014 round 4 matched theorems only, so a `def : False` passed) in the eight certificate modules AND in Audit.lean itself (the auditor is not exempt). Binding digest: check.sh binds to the SHA-256 of a canonical AUDIT-MANIFEST block covering the POLICY constants (allowedBoundary + certModules \u2014 round-5 NEW-1: widening allowedBoundary previously re-opened the False-proof with the fingerprint byte-identical), every certificate's fully-elaborated statement, and every reachable specification definition's fully-elaborated BODY (round-5 NEW-2: redefining a reference fold to *be* the extracted loop previously left cone and fingerprint intact while the certificate degenerated to `loop = loop`). The 32-bit Expr.hash is retained only as a per-certificate diagnostic, not as the binding. Fail-closed; adversarially exercised by check-selftest.sh. check.sh Phase 0 additionally purges stale .olean files, forbids stray .lean outside gen/ and Proofs/, and pins model + harness bytes."
-}
+}
\ No newline at end of file
diff --git a/verification/check.sh b/verification/check.sh
index e39f617..3a42508 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -57,12 +57,25 @@ echo "=== Phase 0: build hygiene + model/harness integrity ==="
 #     (*.olean is .gitignored, so `git status` showed only the import line).
 #     The verdict must depend on COMMITTED BYTES, never on untracked build state.
 find "$HERE" -name '*.olean' -delete 2>/dev/null || true
-#     Aeneas also emits `*_Template.lean` scaffolding into gen/ on every
-#     extraction. Those files are UNTRACKED byproducts (a fresh clone has only
-#     the four pinned model files), nothing imports them, and they would
-#     otherwise sit on LEAN_PATH unpinned — the same untracked-state problem.
-#     Remove them here so the gen/ file-set assertion below can be exact.
-find "$HERE/gen" -name '*_Template.lean' -delete 2>/dev/null || true
+#     Aeneas also emits `*_Template.lean` into gen/ on every extraction. This
+#     script used to DELETE it, reasoning that an untracked file sitting on
+#     LEAN_PATH is exactly the unpinned-state problem described above. The
+#     reasoning was right; the remedy was the weaker of the two available. The
+#     ed25519 forks face the identical choice and COMMIT AND PIN their
+#     templates, which removes the untracked state just as completely and keeps
+#     the evidence.
+#
+#     The evidence matters. The template is Aeneas's own statement of what the
+#     extracted Rust needs from outside, and it is the ONLY artifact against
+#     which "does the hand-written model ANSWER the extraction?" can be asked.
+#     Deleting it made that question unaskable, which is why this repository
+#     shipped a Template/model pair with no correspondence check at all —
+#     round-8 estate review (GPT-5.6). It is now committed, pinned in
+#     model_integrity_sha256 like every other model file, and consumed by
+#     Phase 0d below.
+#
+#     It still never joins the environment: Phase 1 compiles the named model
+#     modules, not a glob, and nothing imports the template.
 # (b) No Lean source OR compiled module may sit outside gen/ and Proofs/;
 #     LEAN_PATH includes $PWD, so either can join the environment ungated.
 STRAY=$(find "$HERE" -maxdepth 1 \( -name '*.lean' -o -name '*.olean' \) -printf '%f\n' 2>/dev/null || true)
@@ -141,6 +154,38 @@ sys.exit(1 if bad else 0)
 PY
 
 # ── Phase 1: model ──────────────────────────────────────────────────────────
+# ── Phase 0d: template/model correspondence ─────────────────────────────────
+# WHAT THE BYTE PINS DO NOT ESTABLISH. Phase 0 pins the model files byte for
+# byte, so they cannot drift unnoticed. It says nothing about whether the model
+# ANSWERS the extraction: Aeneas states, in FunsExternal_Template.lean, exactly
+# what the extracted Rust needs from outside, and each such name must be
+# provided by the hand-written sibling FunsExternal.lean or by a real definition
+# in the proven corpus. A name the extraction asks for and nothing supplies is
+# drift the byte pins cannot see, because both files are individually pinned and
+# individually unchanged.
+#
+# This repository had a Template/model pair and NO correspondence check at all
+# — round-8 estate review (GPT-5.6). The scanner is the one the ed25519 forks
+# use, including its two round-8 corrections: a named Lean `section` does NOT
+# qualify declaration names (treating it as a namespace made the scanner invent
+# `Foo.bar`, and a semantic phase then certified an unrelated `Foo.bar` while
+# the real external went unqueried), and an EXTRA AXIOM in the model — an
+# assumption no template asks for — is a failure rather than a silent row.
+echo "=== Phase 0d: template/model correspondence ==="
+CORR=$(python3 "$HERE/model-correspondence.py" "$HERE") || {
+  echo "MODEL CORRESPONDENCE FAILED — the extraction asks for something this"
+  echo "repository does not supply, or the model declares an axiom nothing asks for."
+  printf '%s\n' "$CORR" | grep -E 'UNRESOLVED|EXTRA-AXIOM' | sed 's/^/    /'
+  exit 1
+}
+if ! printf '%s\n' "$CORR" | cmp -s - "$HERE/MODEL-CORRESPONDENCE.txt"; then
+  echo "MODEL CORRESPONDENCE FAILED — the committed table is not what the"
+  echo "scanner now produces. Differences:"
+  diff <(printf '%s\n' "$CORR") "$HERE/MODEL-CORRESPONDENCE.txt" | head -20 | sed 's/^/    /'
+  exit 1
+fi
+echo "  $(grep -c '|MODEL$\||PROVEN$' "$HERE/MODEL-CORRESPONDENCE.txt") externals, every one answered by the pinned model"
+
 echo "=== Phase 1: compile the extracted model ==="
 cd "$AENEAS_LEAN"
 lake env bash -c "
diff --git a/verification/gen/SlhVerify/FunsExternal_Template.lean b/verification/gen/SlhVerify/FunsExternal_Template.lean
new file mode 100644
index 0000000..4e57dd7
--- /dev/null
+++ b/verification/gen/SlhVerify/FunsExternal_Template.lean
@@ -0,0 +1,103 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [fips205]: external functions.
+-- This is a template file: rename it to "FunsExternal.lean" and fill the holes.
+import Aeneas
+import SlhVerify.Types
+open Aeneas Aeneas.Std Result ControlFlow Error
+set_option linter.dupNamespace false
+set_option linter.hashCommand false
+set_option linter.unusedVariables false
+
+/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
+set_option maxHeartbeats 1000000
+
+/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
+set_option maxRecDepth 2048
+open fips205
+
+/-- [core::iter::range::{impl core::iter::range::Step for u32}::backward_checked]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 290:16-290:74
+    Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::backward_checked]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<u32>}::backward_checked"]
+axiom U32.Insts.CoreIterRangeStep.backward_checked
+  : Std.U32 → Std.Usize → Result (Option Std.U32)
+
+/-- [core::iter::range::{impl core::iter::range::Step for u32}::forward_checked]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 282:16-282:73
+    Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::forward_checked]
+    Visibility: public -/
+@[rust_fun
+  "core::iter::range::{core::iter::range::Step<u32>}::forward_checked"]
+axiom U32.Insts.CoreIterRangeStep.forward_checked
+  : Std.U32 → Std.Usize → Result (Option Std.U32)
+
+/-- [core::iter::range::{impl core::iter::range::Step for u32}::steps_between]:
+    Source: '/rustc/library/core/src/iter/range.rs', lines 271:16-271:84
+    Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::steps_between]
+    Visibility: public -/
+@[rust_fun "core::iter::range::{core::iter::range::Step<u32>}::steps_between"]
+axiom U32.Insts.CoreIterRangeStep.steps_between
+  : Std.U32 → Std.U32 → Result (Std.Usize × (Option Std.Usize))
+
+/-- [zeroize::{impl zeroize::Zeroize for Z}::zeroize]:
+    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 274:4-274:25
+    Name pattern: [zeroize::{zeroize::Zeroize<@Z>}::zeroize]
+    Visibility: public -/
+@[rust_fun "zeroize::{zeroize::Zeroize<@Z>}::zeroize"]
+axiom zeroize.Zeroize.Blanket.zeroize
+  {Z : Type} (DefaultIsZeroesInst : zeroize.DefaultIsZeroes Z) : Z → Result Z
+
+/-- [zeroize::{impl zeroize::Zeroize for [Z; N]}::zeroize]:
+    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 346:4-346:25
+    Name pattern: [zeroize::{zeroize::Zeroize<[@Z; @N]>}::zeroize]
+    Visibility: public -/
+@[rust_fun "zeroize::{zeroize::Zeroize<[@Z; @N]>}::zeroize"]
+axiom Array.Insts.ZeroizeZeroize.zeroize
+  {Z : Type} {N : Std.Usize} (ZeroizeInst : zeroize.Zeroize Z) :
+  Array Z N → Result (Array Z N)
+
+/-- [zeroize::__internal::{impl zeroize::__internal::AssertZeroize for T}::zeroize_or_on_drop]:
+    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 846:8-846:40
+    Name pattern: [zeroize::__internal::{zeroize::__internal::AssertZeroize<@T>}::zeroize_or_on_drop]
+    Visibility: public -/
+@[rust_fun
+  "zeroize::__internal::{zeroize::__internal::AssertZeroize<@T>}::zeroize_or_on_drop"]
+axiom zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
+  {T : Type} (ZeroizeInst : zeroize.Zeroize T) : T → Result T
+
+/-- [fips205::verify_mono::oracle::f]:
+    Source: 'src/verify_mono.rs', lines 49:4-51:5 -/
+axiom verify_mono.oracle.f
+  (N : Std.Usize) :
+  Slice Std.U8 → types.Adrs → Slice Std.U8 → Result (Array Std.U8 N)
+
+/-- [fips205::verify_mono::oracle::h]:
+    Source: 'src/verify_mono.rs', lines 54:4-56:5 -/
+axiom verify_mono.oracle.h
+  (N : Std.Usize) :
+  Slice Std.U8 → types.Adrs → Slice Std.U8 → Slice Std.U8 → Result
+    (Array Std.U8 N)
+
+/-- [fips205::verify_mono::oracle::t_l]:
+    Source: 'src/verify_mono.rs', lines 60:4-64:5 -/
+axiom verify_mono.oracle.t_l
+  {X : Std.Usize} {N : Std.Usize} :
+  Slice Std.U8 → types.Adrs → Array (Array Std.U8 N) X → Result (Array
+    Std.U8 N)
+
+/-- [fips205::verify_mono::oracle::t_len]:
+    Source: 'src/verify_mono.rs', lines 69:4-73:5 -/
+axiom verify_mono.oracle.t_len
+  {X : Std.Usize} {N : Std.Usize} :
+  Slice Std.U8 → types.Adrs → Array (Array Std.U8 N) X → Result (Array
+    Std.U8 N)
+
+/-- [fips205::verify_mono::oracle::h_msg]:
+    Source: 'src/verify_mono.rs', lines 81:4-85:5 -/
+axiom verify_mono.oracle.h_msg
+  (M : Std.Usize) :
+  Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Result
+    (Array Std.U8 M)
+
diff --git a/verification/model-correspondence.py b/verification/model-correspondence.py
new file mode 100755
index 0000000..ba9f810
--- /dev/null
+++ b/verification/model-correspondence.py
@@ -0,0 +1,259 @@
+#!/usr/bin/env python3
+"""Classify every external the extraction declares.
+
+For each gen/<dir>/<X>_Template.lean, Aeneas states what the extracted Rust
+needs from outside. Each such name must be provided by exactly one of:
+
+  MODEL   — declared in the hand-written sibling gen/<dir>/<X>.lean: an
+            assumption, which the axiom gate and the per-certificate cones
+            then govern;
+  PROVEN  — resolved to a real definition in the proven corpus, because a
+            module of this repository declares it (namespace-aware).
+
+Anything else is drift: the extraction asks for something this repository does
+not provide.
+
+────────────────────────────────────────────────────────────────────────────
+WHY THIS FILE WAS REWRITTEN — 2026-08-01, round-7 external review
+
+The first version matched declarations with a LINE-ORIENTED regex requiring the
+keyword and the name on the same physical line, and it did not strip comments.
+Both assumptions are false about Lean, and false about Aeneas's own output.
+Three of the four forks contain, verbatim:
+
+    axiom
+      curve25519_dalek.edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg
+      :
+      curve25519_dalek.edwards.EdwardsPoint -> Result ...
+
+The old pattern matched nothing there, so that declaration was SILENTLY
+DROPPED: no MODEL row, no PROVEN row, and no failure. Every committed
+MODEL-CORRESPONDENCE.txt was missing it, and every button passed green over the
+incomplete table. A reviewer separately showed that a definition appearing only
+inside a `/- ... -/` comment was read as a real declaration, so the scanner
+could also report PROVEN for a name Lean resolves to an axiom.
+
+The lesson is not "write a better regex". It is that this scanner was
+FAIL-OPEN: input it could not parse produced silence instead of a stop. A gate
+that drops what it cannot read is worse than no gate, because the button prints
+green across the gap and the gap is invisible in the diff.
+
+This version therefore:
+  · strips comments first, including NESTED `/- ... -/` blocks, which Lean has
+    and which a non-greedy match would close at the first inner `-/`;
+  · allows a declaration's name to appear on a later line than its keyword;
+  · tracks `namespace` / `section` / `end` over the stripped text;
+  · FAILS CLOSED — every declaration keyword must yield a name, or the scanner
+    exits non-zero naming file and line. Nothing is dropped, ever.
+
+WHAT IT STILL IS NOT. This is a source scanner, not a semantic Lean query. It
+cannot see `export`, aliases, or how Lean actually resolves a name at
+elaboration. A PROVEN row is documentary evidence about the extraction
+boundary; it is NOT a Lean-checked fact, and the trust documents must not claim
+it is. What the estate relies on for soundness is kernel-side and
+environment-derived — Phase 2b's axiom gate, Phase 2c's inventory, and the
+exact per-certificate cones of Phase 3/3b — none of which consult this file.
+────────────────────────────────────────────────────────────────────────────
+"""
+import re
+import sys
+import os
+import glob
+
+KEYWORDS = ('axiom', 'def', 'abbrev', 'opaque', 'structure', 'inductive',
+            'instance', 'theorem', 'lemma')
+
+# A declaration keyword opening a logical line, after any attributes and
+# modifiers. The NAME is deliberately NOT part of this pattern: it may sit on a
+# later line, which is precisely the case the previous scanner dropped.
+KW = re.compile(
+    r'^[ \t]*(?:@\[[^\]]*\][ \t\n]*)*'
+    r'(?:private |protected |noncomputable |unsafe |partial |scoped |local )*'
+    r'(' + '|'.join(KEYWORDS) + r')(?=[ \t\n])',
+    re.M)
+
+IDENT = re.compile(r"[ \t\n]*([A-Za-z_][A-Za-z0-9_.'!?]*)")
+
+NS = re.compile(
+    r"^[ \t]*(namespace|section|end)(?:[ \t]+([A-Za-z_][A-Za-z0-9_.']*))?[ \t]*$",
+    re.M)
+
+
+class ScanError(Exception):
+    """Raised when a declaration cannot be parsed. Never swallowed."""
+
+
+def strip_comments(text):
+    """Remove Lean comments, preserving newlines so line numbers stay true.
+
+    Block comments NEST in Lean, so this needs a depth counter: a non-greedy
+    `/-.*?-/` would close the outer block at the first inner `-/` and leave the
+    tail of a nested comment looking like source.
+    """
+    out, i, n, depth = [], 0, len(text), 0
+    while i < n:
+        if text.startswith('/-', i):
+            depth += 1
+            out.append('  ')
+            i += 2
+            continue
+        if text.startswith('-/', i):
+            if depth:
+                depth -= 1
+            out.append('  ')
+            i += 2
+            continue
+        if depth:
+            out.append('\n' if text[i] == '\n' else ' ')
+            i += 1
+            continue
+        if text.startswith('--', i):
+            j = text.find('\n', i)
+            if j < 0:
+                out.append(' ' * (n - i))
+                break
+            out.append(' ' * (j - i))
+            i = j
+            continue
+        out.append(text[i])
+        i += 1
+    return ''.join(out)
+
+
+def declared(path):
+    """{fully-qualified name: declaration keyword} for one file.
+
+    Returns a MAPPING, not a set, because the keyword is load-bearing: an
+    `axiom` the template never asks for must stop the button, while an extra
+    `def` is an ordinary helper. Callers that only need names take `set(...)`.
+
+    Raises ScanError on any declaration keyword whose name cannot be read.
+    """
+    raw = open(path, encoding='utf-8', errors='replace').read()
+    text = strip_comments(raw)
+
+    # Scope events by offset, so each declaration can be placed in its stack.
+    events = [(m.start(), m.group(1), m.group(2)) for m in NS.finditer(text)]
+
+    names = {}
+    for m in KW.finditer(text):
+        im = IDENT.match(text, m.end())
+        if not im:
+            line = text.count('\n', 0, m.start()) + 1
+            raise ScanError(
+                "%s:%d: `%s` with no parseable name. This scanner fails closed:"
+                " it will not drop a declaration it cannot read."
+                % (path, line, m.group(1)))
+        stack = []
+        for off, kind, arg in events:
+            if off > m.start():
+                break
+            if kind == 'namespace':
+                stack.append(arg)
+            elif kind == 'section':
+                # A NAMED SECTION DOES NOT QUALIFY DECLARATION NAMES. `section
+                # Foo` opens a scope for `variable`/`open` and gives `end Foo` a
+                # label to match; it does not make `bar` into `Foo.bar`. This
+                # line pushed `arg`, so a template reading
+                #     section Foo
+                #     axiom bar : Nat
+                #     end Foo
+                # was reported as declaring `Foo.bar`. Round-8 review (GPT-5.6,
+                # register key `section-prefix-bug`) showed the consequence:
+                # `--names` handed Phase 2d only `Foo.bar`, Lean happily
+                # resolved an unrelated `Foo.bar` definition elsewhere in the
+                # corpus and returned PROVEN, and the axiom the extraction
+                # ACTUALLY depends on was never queried at all. The scanner had
+                # been rewritten that same week specifically to be fail-closed.
+                # None appends a frame so `end` still balances, and the
+                # comprehension below drops it from the prefix.
+                stack.append(None)
+            elif stack:
+                stack.pop()
+        prefix = [p for p in stack if p]
+        full = '.'.join(prefix + [im.group(1)]) if prefix else im.group(1)
+        names.setdefault(full, m.group(1))
+    return names
+
+
+def main(root):
+    gen = os.path.join(root, 'gen')
+    templates = sorted(glob.glob(os.path.join(gen, '*', '*_Template.lean')))
+    # The proven corpus: every generated module that is neither a template nor
+    # a hand-written model. These are the files Aeneas produced from Rust.
+    models = {t.replace('_Template', '') for t in templates}
+    corpus = set()
+    for f in sorted(glob.glob(os.path.join(gen, '*', '*.lean'))):
+        if f in models or f.endswith('_Template.lean'):
+            continue
+        corpus.update(declared(f))
+
+    rows, unresolved = [], []
+    for t in templates:
+        model = t.replace('_Template', '')
+        rel = os.path.relpath(t, gen).replace('_Template.lean', '')
+        tnames = set(declared(t))
+        mkinds = declared(model) if os.path.exists(model) else {}
+        mnames = set(mkinds)
+        for n in sorted(tnames):
+            if n in mnames:
+                rows.append(f'{rel}|{n}|MODEL')
+            elif n in corpus:
+                rows.append(f'{rel}|{n}|PROVEN')
+            else:
+                rows.append(f'{rel}|{n}|UNRESOLVED')
+                unresolved.append(f'{rel}|{n}')
+        # AN EXTRA AXIOM IS A FAILURE, and this is the second half of the
+        # round-8 section-prefix finding. EXTRA was the one verdict that could
+        # not fail: the model declares something the template did not ask for.
+        # When the scanner mis-derived the template's name (`Foo.bar` instead of
+        # `bar`), the axiom the extraction ACTUALLY depends on did not vanish —
+        # it landed here, as a harmless-looking EXTRA row, while the invented
+        # name was certified PROVEN. A silent bucket next to a fail-closed
+        # parser is just a slower way of dropping things.
+        #
+        # There is no benign reading of an extra AXIOM either way. The model
+        # exists to answer the template; an assumption nothing asks for is
+        # either a parse the scanner got wrong or an unaudited assumption
+        # nobody is governing. Both must stop the button. Extra non-axiom
+        # declarations stay reportable-but-tolerated: helper definitions in a
+        # model file are ordinary.
+        for n in sorted(mnames - tnames):
+            kind = mkinds.get(n, '')
+            if kind == 'axiom':
+                rows.append(f'{rel}|{n}|EXTRA-AXIOM')
+                unresolved.append(f'{rel}|{n} (axiom in the model that no '
+                                  f'template external asks for)')
+            else:
+                rows.append(f'{rel}|{n}|EXTRA')
+    print('\n'.join(rows))
+    print(f'CORRESPONDENCE-COUNT|{len(rows)}')
+    return 1 if unresolved else 0
+
+
+def emit_names(root):
+    """Every name the EXTRACTION asks for, as `<rel>|<name>`.
+
+    Template discovery is unavoidably textual: the template is not imported (it
+    would clash with the model, which declares the same names), so no Lean
+    environment contains it. That is why `declared()` fails closed — this list
+    is the input to the semantic phase, and a name missing here is a name
+    nothing will ever check.
+    """
+    gen = os.path.join(root, 'gen')
+    for t in sorted(glob.glob(os.path.join(gen, '*', '*_Template.lean'))):
+        rel = os.path.relpath(t, gen).replace('_Template.lean', '')
+        for n in sorted(declared(t)):
+            print(f'{rel}|{n}')
+    return 0
+
+
+if __name__ == '__main__':
+    try:
+        if len(sys.argv) > 2 and sys.argv[1] == '--names':
+            sys.exit(emit_names(sys.argv[2]))
+        sys.exit(main(sys.argv[1]))
+    except ScanError as e:
+        # Fail closed and loudly. Never degrade to a partial table.
+        print('MODEL CORRESPONDENCE SCAN FAILED: %s' % e, file=sys.stderr)
+        sys.exit(2)