diff --git a/verification/HARNESS.sha256 b/verification/HARNESS.sha256
index d9c4152..02eb375 100644
--- a/verification/HARNESS.sha256
+++ b/verification/HARNESS.sha256
@@ -1,5 +1,5 @@
 e7d422f0be9a9e6f5465058292e30c711d52856428da2b01c470a57ec181540c  AUDIT-MANIFEST.txt
-91ab3fce14a03fc6fd12b3cdbb52cd0f0e379ae2cd564ec7b61d339d4616fd32  check.sh
+857a92d50d44c5fe4db2bfdb4fc3a28f7b345b369414a140a66298fd6ff1b0fe  check.sh
 070147e2667053bd5d5e1174b969fc6c91bfcf15ded1a5bff57754e15f416885  fidelity/lean_defs.py
 5d82462a002ac9fc782e95afe78b7719ba64b6410b5d2bfa620fe5317367dbf2  fidelity/run_fidelity.py
 503babb3f4e6aff82ebd59e8752469ecd60fba440ed3b11b3f97c2b655fbd9bf  gen/LTLAcc/HashExternal.lean
@@ -10,6 +10,6 @@ ce4c4e3d87434b9663f46de25ce34b48a0cf0d392e0a320a0787b4674a2d7b61  lean-toolchain
 eda93f520546a692926b2a46bcb79332e1795879e5083327a8bf2404aca5cf87  Proofs/AxiomCheck.lean
 de5cdf01724fd4333b0652769bfede3ee150fedfa0a6c4ffbc8e7ab065843928  Proofs/Inventory.lean
 0b8a0fc6947af1d1e600a756eb2b07dc88d189b21df3220c4501a41be8b33f1e  run_bare.sh
-dd975f4682035fe3313ce85b70f1aa1e411f9534ff62a29f5591630859c55a75  selftest_audit.sh
+473e2463d9c26653c8435ad6758044742f200eb13ea0db4b8f076466c08bd87a  selftest_audit.sh
 3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6  selftest-harness.sh
 cf6d4d8210e224a054d4ab693c28c83e7a9ddebda05da47d6ec311d825a606c0  selftest_statements.sh
diff --git a/verification/check.sh b/verification/check.sh
index f52784c..bee6e8b 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -300,6 +300,124 @@ lake env bash -c "
 " > "$INVLOG" 2>&1 || { cat "$INVLOG"; echo "INVENTORY COMPILE FAILED"; exit 1; }
 "$HERE/inventory_gate.sh" "$INVLOG" "$HERE/inventory-allowlist.txt" || COVFAIL=1
 
+# ── Phase 3b-kernel: kernel-side axiom-declaration gate ─────────────────────
+# PORTED FROM THE ed25519 FORKS after round-7 review (Claude, finding F2).
+#
+# What this repository had: a SOURCE-TEXT axiom grep in Phase 1, and an
+# environment walk in Phase 3b that runs inside Inventory.lean. Both have the
+# same blind spot from opposite directions. The grep misses ` axiom c : ...`
+# with a leading space — this repo's own selftest_audit.sh case 12 exploits
+# exactly that. And the environment walk is an `#eval`: a declaration placed
+# AFTER it in the same file exists in the compiled object file but not in the
+# environment when the walk runs, so the button reported "no axiom, no claim"
+# over a claim that was sitting in the environment, with the statement digest
+# byte-identical. A reviewer demonstrated it.
+#
+# The fix is the one the forks already carry: ask the KERNEL, by reading every
+# compiled object file directly. readModuleData sees what was actually stored,
+# regardless of indentation, attributes, privacy, or where in the file a
+# declaration sits relative to any #eval. Membership self-derives from the
+# manifest, so a new module cannot escape by being unlisted, and the module
+# count must match so a deleted .olean cannot make the scan vacuous.
+# PLACEMENT. This deliberately runs INSIDE Phase 3b rather than beside the
+# compile phase, unlike the ed25519 forks. There the audit drivers are members
+# of the compile manifest, so they exist by the time the kernel gate runs. Here
+# they are not: AxiomCheck is compiled by Phase 3 and Inventory by Phase 3b, so
+# an earlier gate would fail on a missing artifact — which it did, correctly,
+# when this was first ported. It must run after both drivers exist, because the
+# instruments are exactly what it has to see.
+echo "=== Phase 3b-kernel: kernel-side axiom-declaration gate ==="
+KERNLOG=$(mktemp /tmp/acc-kernel-XXXX.log)
+AXGATE=$(mktemp "$HERE/.axgate-XXXX.lean")
+ALL_MODULES=$(printf '"%s.olean", ' "${PROOFS[@]}" "${DRIVERS[@]}" | sed 's/, $//')
+cat > "$AXGATE" <<LEANGATE
+import Lean
+open Lean System
+#eval show CoreM Unit from do
+  let dir : FilePath := "$HERE/Proofs"
+  let expected : List String := [$ALL_MODULES]
+  let mut errs : Array String := #[]
+  let mut nConst := 0
+  let mut nMod := 0
+  let mut seen : Std.HashSet Name := {}
+  for name in expected do
+    let p := dir / name
+    -- FAIL CLOSED ON ABSENCE: a missing artifact would make this scan vacuous
+    -- for that module, so it is an error and never a skip.
+    unless (← p.pathExists) do
+      throwError "MISSING ARTIFACT: {p} — the kernel gate would be vacuous for it"
+    let (mod, _) ← readModuleData p
+    nMod := nMod + 1
+    for ci in mod.constants do
+      nConst := nConst + 1
+      seen := seen.insert ci.name
+      if ci matches .axiomInfo _ then
+        errs := errs.push s!"  {name}: {ci.name}"
+  unless errs.isEmpty do
+    throwError "AXIOM DECLARED under Proofs/ (kernel-side gate):\n{String.intercalate "\n" errs.toList}"
+  logInfo s!"  kernel confirms: {nConst} declarations across {nMod} compiled modules, none is an axiom"
+  for n in seen do IO.println s!"KERNEL-NAME|{n}"
+LEANGATE
+cd "$AENEAS_LEAN"
+AXGATE_RC=0
+lake env bash -c "
+  set -euo pipefail
+  cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
+  cd '$HERE'
+  LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' '$AXGATE'
+" 2>&1 | tee "$KERNLOG" || AXGATE_RC=${PIPESTATUS[0]}
+cd "$HERE"
+rm -f "$AXGATE" "${AXGATE%.lean}.olean"
+if [ "$AXGATE_RC" -ne 0 ]; then
+  echo "AXIOM SMUGGLING GATE FAILED (kernel-side) — see the error above."
+  rm -f "$KERNLOG" "$INVLOG"; exit 1
+fi
+echo ""
+
+# ── THE ACCOUNTING IDENTITY ─────────────────────────────────────────────────
+# Ported from the ed25519 forks, and the reason it is here is a demonstrated
+# attack, not symmetry. A reviewer appended to Proofs/Inventory.lean, AFTER the
+# `#eval` that performs the driver walk:
+#
+#     def bait : Nat := 0
+#     theorem bait.smuggled : ... := ...
+#
+# re-pinned, and ran the button. It printed "no axiom, no claim", the statement
+# digest was byte-identical to the clean tree, and the run went green — while a
+# theorem with a real axiom cone sat in the compiled environment. It was in
+# neither walk: not corpus, because an instrument is not corpus; not driver
+# surface, because it post-dates the emitter that reports the driver surface.
+#
+# The two walks read ENVIRONMENTS. Phase 2b reads OBJECT FILES. What a walk
+# cannot see because of where it sits in a file, the object file still holds.
+# So the property enforced here is containment, and it is what closes the hole:
+#
+#     every constant the kernel sees  ⊆  corpus inventory ∪ instrument surface
+#
+# Compared as SETS, deliberately. Counts cannot express this relation: an
+# object file may hold two physical copies of one lazily-materialised equation
+# lemma, while an environment holds one constant per name — arithmetic between
+# those views misled the ed25519 version of this check twice before it was
+# stated as containment.
+KERN_NAMES=$(mktemp /tmp/acc-kernnames-XXXX.txt)
+ACCT_NAMES=$(mktemp /tmp/acc-acctnames-XXXX.txt)
+LC_ALL=C grep '^KERNEL-NAME|' "$KERNLOG" | cut -d'|' -f2 | LC_ALL=C sort -u > "$KERN_NAMES"
+{ LC_ALL=C awk -F'|' '/^INV\|/{print $2}' "$INVLOG"
+  LC_ALL=C grep '^DRV|' "$INVLOG" | cut -d'|' -f2
+} | LC_ALL=C sort -u > "$ACCT_NAMES"
+UNACCOUNTED=$(LC_ALL=C comm -23 "$KERN_NAMES" "$ACCT_NAMES")
+if [ ! -s "$KERN_NAMES" ]; then
+  echo "  ACCOUNTING FAILED: Phase 2b reported no constant names — the scan was vacuous"
+  COVFAIL=1
+elif [ -n "$UNACCOUNTED" ]; then
+  echo "  ACCOUNTING FAILED: the kernel holds constants that neither walk accounts for:"
+  printf '%s\n' "$UNACCOUNTED" | head -20 | sed 's/^/    /'
+  COVFAIL=1
+else
+  echo "  accounting: every one of $(wc -l < "$KERN_NAMES") kernel constants is covered by the corpus inventory or the instrument surface"
+fi
+rm -f "$KERN_NAMES" "$ACCT_NAMES" "$KERNLOG"
+
 # The inventory's corpus-module list must BE the compile manifest — both
 # directions, so neither can drift from the other silently.
 # Read the module LISTS, not the file. This comparison used to grep the whole
diff --git a/verification/selftest_audit.sh b/verification/selftest_audit.sh
index 609b88e..0953774 100755
--- a/verification/selftest_audit.sh
+++ b/verification/selftest_audit.sh
@@ -248,6 +248,55 @@ grep -q "DRIVER SURFACE VIOLATION" "$T/check13.out" || {
 echo "  ✓ case 13 standalone claim in the axiom-check driver: DRIVER SURFACE VIOLATION"
 cp "$SRC/Proofs/AxiomCheck.lean" "$T/Proofs/AxiomCheck.lean"
 
+# Case 13 restores Proofs/AxiomCheck.lean but not its PIN, which it rewrote to
+# match the tampered file. Harmless while 13 was last; case 14 runs check.sh and
+# would die in Phase 0c on that stale pin. Re-pin here rather than in case 13,
+# so that case keeps testing exactly what it tested before. (Second instance of
+# this residue pattern in this file — see the note above case 10.)
+( cd "$T" && grep -v ' Proofs/AxiomCheck.lean$' HARNESS.sha256 > .h \
+  && sha256sum Proofs/AxiomCheck.lean >> .h && sort -k2 -o .h .h && mv .h HARNESS.sha256 )
+
+# 14 — A DECLARATION THAT POST-DATES THE WALK THAT REPORTS IT.
+#      Round-7 review (Claude, finding F2), reproduced verbatim. The driver
+#      surface is reported by an `#eval` inside Proofs/Inventory.lean.
+#      Anything declared AFTER that command exists in the compiled object file
+#      but not in the environment while the command runs, so the walk cannot
+#      see it. Before Phase 3b-kernel existed this went GREEN: the button
+#      printed "no axiom, no claim", the statement digest was byte-identical
+#      to the clean tree, and a theorem with a real axiom cone sat in the
+#      environment — in neither walk, in no allowlist, pinned by nothing.
+#
+#      The kernel reads OBJECT FILES, so it sees what an environment walk
+#      placed mid-file cannot. That is the whole point of the containment
+#      check, and this case is the reason it exists.
+#      NOTE ON THE PAYLOAD. `theorem bait.smuggled : True := trivial` does NOT
+#      work here, and the reason is worth keeping: Phase 1's stub audit greps
+#      for `: True :=` and catches it first. That is real defence in depth, but
+#      it means the naive payload never reaches the gate under test. The one
+#      below is the reviewer's original — a genuine claim with a real cone,
+#      invisible to every source-text check — so this case exercises the
+#      accounting identity and nothing else.
+cat >> "$T/Proofs/Inventory.lean" <<'BAIT'
+
+def bait : Nat := 0
+theorem bait.smuggled : ∀ n : Nat, n + 0 = n := by
+  have _h := Classical.em True
+  intro n; simp
+BAIT
+( cd "$T" && grep -v ' Proofs/Inventory.lean$' HARNESS.sha256 > .h \
+  && sha256sum Proofs/Inventory.lean >> .h && sort -k2 -o .h .h && mv .h HARNESS.sha256 )
+if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check14.out" 2>&1; then
+  echo "  ✗ case 14: check.sh PASSED with a declaration appended after the driver walk"; exit 1
+fi
+grep -q "ACCOUNTING FAILED" "$T/check14.out" \
+  && grep -q "bait" "$T/check14.out" || {
+  echo "  ✗ case 14: failed, but not with the accounting diagnosis naming the declaration"
+  tail -8 "$T/check14.out"; exit 1; }
+echo "  ✓ case 14 declaration after the driver walk: ACCOUNTING FAILED names it"
+cp "$SRC/Proofs/Inventory.lean" "$T/Proofs/Inventory.lean"
+( cd "$T" && grep -v ' Proofs/Inventory.lean$' HARNESS.sha256 > .h \
+  && sha256sum Proofs/Inventory.lean >> .h && sort -k2 -o .h .h && mv .h HARNESS.sha256 )
+
 rm -rf "$WORK"
 trap - ERR
-echo "=== SELF-TEST GREEN: 14 attack cases defeated + positive control ==="
+echo "=== SELF-TEST GREEN: 15 attack cases defeated + positive control ==="