diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml
index c276766..63587b9 100644
--- a/.github/workflows/proof-safety.yml
+++ b/.github/workflows/proof-safety.yml
@@ -64,3 +64,40 @@ jobs:
           ECHIDNA_BIN: ${{ github.workspace }}/_echidna/target/debug/echidna
         run: |
           bash tests/e2e.sh
+  agda:
+    # DOM-1/DOM-2 (Agda theory). The check-run name agda-proofs is the
+    # contract echidna's W0 gate (check 12) reads. PROOF-POLICY §2.1 invocation with the
+    # pinned Agda 2.7.0.1 and agda-stdlib 2.1 (digests in setup-agda.sh),
+    # then the §8.2 cone receipt each theorem's PWG is derived from. A
+    # missing or wrong toolchain fails the job; it never skips.
+    name: agda-proofs
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - name: Install pinned Agda and standard library
+        run: bash scripts/ci/setup-agda.sh
+      - name: Type-check under the §2.1 invocation (through the wrapper)
+        run: |
+          set -euo pipefail
+          stdlib_src="$(dirname "$(head -n 1 "$AGDA_LIBRARIES_FILE")")/src"
+          AGDA_LIBRARY_INCLUDE="$stdlib_src" bash scripts/agda-safe-check.sh \
+            verification/proofs/agda/Burrow/Trust.agda verification/proofs/agda/Burrow/Ledger.agda
+      - name: Record the §8.2 cone receipts
+        env:
+          AGDA_STDLIB_SHA256: 72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431
+        run: |
+          set -euo pipefail
+          bash scripts/ci/test-agda-cone-receipt.sh
+          receipts="$RUNNER_TEMP/agda-cone-receipts.jsonl"
+          : > "$receipts"
+          for m in Burrow/Trust.agda Burrow/Ledger.agda; do
+            (cd verification/proofs/agda && bash ../../../scripts/ci/agda-cone-receipt.sh "$m") >> "$receipts"
+          done
+          cat "$receipts"
+          {
+            echo '## PROOF-POLICY §8.2 cone receipts (DOM-1, DOM-2)'
+            jq -r '"\(.source.entrypoint) at \(.source.commit): \(.toolchain.agda), \(.import_cone.count) modules, scan \(.postulate_scan.result)"' "$receipts"
+          } >> "$GITHUB_STEP_SUMMARY"
diff --git a/CLAUDE.md b/CLAUDE.md
index dab6e6d..8581a2f 100644
--- a/CLAUDE.md
+++ b/CLAUDE.md
@@ -45,7 +45,7 @@ file, not this summary.
 
 | Obligation | Verifier |
 |------------|----------|
-| First-party Rust (`burrower-core`, `-cli`, `-wasm`) | Creusot |
+| First-party Rust (`burrower-core`, `-cli`, `-wasm`) | Creusot with Pearlite contracts, and Verus (§1.2) |
 | APIs, ABIs, wire formats, engineering properties | Idris2 |
 | Theory (anything true of any implementation) | Agda, rechecked in Rocq and Lean |
 
@@ -53,10 +53,14 @@ file, not this summary.
   `agda --safe --without-K --cubical-compatible <module.agda>`.
   `--cubical-compatible` is not full `--cubical`. Pin and record the Agda
   version and standard library with each source commit and proof result.
-- Grade ladder (Mathesis §5): Grade 3 = type-checks locally in Agda,
-  untranslated; 2i = one independent system; 2ii = two, the second
-  non-DTT (e.g. Isabelle/HOL); 1 = machine-checked via a verified checker
-  API in headless CI. Never flatten this into a confidence percentage.
+- Proof grades are PROOF-POLICY §8 *Proof Witness Grades*, weakest to
+  strongest, always with the
+  prefix: `PWG-3` (Agda checks under §2.1, with a receipt) < `PWG-2i` (one
+  Rocq or Lean leg, kernel-checked and RECONCILED) < `PWG-2ii` (both legs)
+  < `PWG-1` (per-commit receipts from a pinned headless checker). A non-DTT
+  witness such as Isabelle/HOL is the tag `+foundation-diverse`, not a
+  grade. Grades are derived from receipts, never asserted. Report a census
+  with its denominator, never a percentage.
 - Missing tools, incompatible dependencies or failed theorems are open
   obligations. Do not skip proofs or weaken flags to make a check green.
 - Escape hatches follow `docs/TRUSTED-BASE-REDUCTION-POLICY.adoc` and are
@@ -64,7 +68,8 @@ file, not this summary.
 - An ECHIDNA result is *evidence about someone else's proof*. Burrower
   records the grade it was told and never asserts one it derived.
 
-Status for this repo: 0 of 7 obligations proven; no first-party Agda
-theorem yet, so nothing here is at Grade 3. See
+Status for this repo: DOM-1 and DOM-2 (Agda theory) are `PWG-3` (2 of 2),
+derived from `docs/reports/2026-11-09-agda-cone-receipts.jsonl`; no Rocq or
+Lean leg yet. See
 `docs/status/PROOF-STATUS.adoc` and
 `docs/reports/audit/2026-11-01-echidna-topology-audit.adoc`.
diff --git a/Justfile b/Justfile
index b40ae3e..07ba456 100644
--- a/Justfile
+++ b/Justfile
@@ -1351,8 +1351,10 @@ proof-check-idris2:
     set -euo pipefail
     echo "=== Checking Idris2 proofs ==="
     if ! command -v idris2 &>/dev/null; then
-        echo "SKIP: idris2 not installed"
-        exit 0
+        # A missing prover is an open obligation, never a pass
+        # (PROOF-POLICY §2.1: do not skip proofs to make a check green).
+        echo "NOT RUN: idris2 not installed"
+        exit 1
     fi
     ERRORS=0
     for f in $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null); do
@@ -1376,8 +1378,10 @@ proof-check-lean4:
     set -euo pipefail
     echo "=== Checking Lean4 proofs ==="
     if ! command -v lean &>/dev/null; then
-        echo "SKIP: lean not installed"
-        exit 0
+        # A missing prover is an open obligation, never a pass
+        # (PROOF-POLICY §2.1: do not skip proofs to make a check green).
+        echo "NOT RUN: lean not installed"
+        exit 1
     fi
     ERRORS=0
     for f in $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null); do
@@ -1401,8 +1405,10 @@ proof-check-agda:
     set -euo pipefail
     echo "=== Checking Agda proofs ==="
     if ! command -v agda &>/dev/null; then
-        echo "SKIP: agda not installed"
-        exit 0
+        # A missing prover is an open obligation, never a pass
+        # (PROOF-POLICY §2.1: do not skip proofs to make a check green).
+        echo "NOT RUN: agda not installed"
+        exit 1
     fi
     # Estate canonical invocation (standards 3-practice/PROOF-POLICY.adoc
     # §2.1). `--cubical-compatible` implies `--without-K`; both are named
@@ -1441,8 +1447,10 @@ proof-check-coq:
     set -euo pipefail
     echo "=== Checking Coq proofs ==="
     if ! command -v coqc &>/dev/null; then
-        echo "SKIP: coqc not installed"
-        exit 0
+        # A missing prover is an open obligation, never a pass
+        # (PROOF-POLICY §2.1: do not skip proofs to make a check green).
+        echo "NOT RUN: coqc not installed"
+        exit 1
     fi
     ERRORS=0
     for f in $(find verification/proofs/coq -name '*.v' 2>/dev/null); do
@@ -1460,26 +1468,10 @@ proof-check-coq:
     fi
     echo "PASS: All Coq proofs verified"
 
-# Scan for dangerous patterns in proof files (believe_me, sorry, Admitted, etc.)
+# Scan proof sources for escape hatches (believe_me, postulate, sorry,
+# Admitted, unsafe pragmas, ...), ignoring comments
 proof-scan-dangerous:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Scanning for dangerous patterns in proofs ==="
-    DANGEROUS=0
-    PATTERNS="believe_me|assert_total|postulate|sorry|Admitted|unsafeCoerce|Obj\.magic"
-    for f in $(find verification/proofs -name '*.idr' -o -name '*.lean' -o -name '*.agda' -o -name '*.v' 2>/dev/null); do
-        MATCHES=$(grep -nE "$PATTERNS" "$f" 2>/dev/null || true)
-        if [ -n "$MATCHES" ]; then
-            echo "  DANGEROUS: $f"
-            echo "$MATCHES" | sed 's/^/    /'
-            DANGEROUS=$((DANGEROUS + 1))
-        fi
-    done
-    if [ "$DANGEROUS" -gt 0 ]; then
-        echo "FAIL: $DANGEROUS file(s) contain dangerous patterns"
-        exit 1
-    fi
-    echo "PASS: No dangerous patterns found in proofs"
+    bash scripts/proof-scan-dangerous.sh verification/proofs
 
 # Show proof status summary
 proof-status:
diff --git a/docs/reports/2026-11-09-agda-cone-receipts.jsonl b/docs/reports/2026-11-09-agda-cone-receipts.jsonl
new file mode 100644
index 0000000..6826bb6
--- /dev/null
+++ b/docs/reports/2026-11-09-agda-cone-receipts.jsonl
@@ -0,0 +1,2 @@
+{"import_cone":{"count":34,"modules":[{"module":"Agda.Builtin.Bool","origin":"agda-kernel","sha256":"514fa25a0df7064cdb213507a0f6332c97288a52d538be3a9df06cc7001ba7f5"},{"module":"Agda.Builtin.Equality","origin":"agda-kernel","sha256":"5735edb0be7e530133814e9431d1466bb1e7892c2a4746c1a0d2a3a0dbea91cd"},{"module":"Agda.Builtin.Maybe","origin":"agda-kernel","sha256":"982f7f2afbfbc4ac41b6bdafddfb5e032a5ddfa71e204f39bbecc23967dc4808"},{"module":"Agda.Builtin.Sigma","origin":"agda-kernel","sha256":"5c393f230b359032f64ff78ad693799a162dbf9cada2089048aedb4c6f669e1f"},{"module":"Agda.Builtin.Unit","origin":"agda-kernel","sha256":"03d06283f9d8005beff99fd42de38b7315aa7697099ea22fc19d060600b16249"},{"module":"Agda.Primitive","origin":"agda-kernel","sha256":"e5e4e04900cf1a28202e2ff26bb20d6fa6401fcc9f4049cd8d14fedd5bd697f8"},{"module":"Burrow.Trust","origin":"first-party","sha256":"5ba1de66b2e4845b7d3663bba338481697e87712cf32da3bb55816da775cce06"},{"module":"Data.Bool.Base","origin":"library","sha256":"124e425ebafee9cbe8fb496b4c8467fdd372b0961ca03e445bfda506738204f6"},{"module":"Data.Empty","origin":"library","sha256":"3a68a9e529c13054202a3892bfcf961bb75db2dc11d63f068189c4cbd48c2cd2"},{"module":"Data.Irrelevant","origin":"library","sha256":"5f225770f471847144eb3908fecb1d4b0a06e7d7b1cb3a12bdebd840bf17a783"},{"module":"Data.Product.Base","origin":"library","sha256":"e2585b0cc6d0c2486cf1f30bd98a3855b00666e8aa8bc0aee5be8253c952a99c"},{"module":"Data.Sum.Base","origin":"library","sha256":"2733ba66eaed94cc0f0b21f2a9ed0533f8a31b5bd487e40384632f1d6204fcfd"},{"module":"Data.Unit","origin":"library","sha256":"320fc4c784fbb6ad847f41ae317f60da346002a119cbca178b2caaa787c2b26c"},{"module":"Data.Unit.Base","origin":"library","sha256":"38cc799f18b6f106336ace8ae66c5a171251c0eb3b6bf32124e33c45d441b2fb"},{"module":"Data.Unit.Polymorphic.Base","origin":"library","sha256":"002ae814be1dafd6f6c4193a2254ee19f7793ffef7dcf1d29f9794db0b19f2a8"},{"module":"Data.Unit.Properties","origin":"library","sha256":"bb9a390596f27739aa9d9c46ef666e42917df4f5000f675ef1042abe3fe2fc62"},{"module":"Function.Base","origin":"library","sha256":"b021bf843c1974a5d50a1a3362f2d6447018629331a3dc2bb0d9ea85ec029e84"},{"module":"Level","origin":"library","sha256":"1168f8373370c10aec0f20bae0cc43db9a34331a49deb4c72efd2574a638a278"},{"module":"Relation.Binary.Bundles","origin":"library","sha256":"fd4b0a832bf9f372d2739668c7e0988e0242519686b69616dc67043923ad88c3"},{"module":"Relation.Binary.Consequences","origin":"library","sha256":"d5f1d178492b9e485a3efdcb16dd18fe623896371e2cae3662d8fde1ff94a455"},{"module":"Relation.Binary.Construct.Composition","origin":"library","sha256":"829ca14501f085b08a0504a61c7874cd20cce07ffc883027ef3465e4f44cf347"},{"module":"Relation.Binary.Core","origin":"library","sha256":"09eda35f4c2f795542f0a2468ade41793e9c9e07889553989e03d343902fcb81"},{"module":"Relation.Binary.Definitions","origin":"library","sha256":"c61495efb42702588229a67461c451dd660bd5d686c244ee1895b9d563547783"},{"module":"Relation.Binary.Properties.Setoid","origin":"library","sha256":"ba05a90fbede6b120c7aefe56944f0c5c772f908a1f60d1644ec4c70c9a93293"},{"module":"Relation.Binary.PropositionalEquality.Core","origin":"library","sha256":"480da0675a0d8ddddcae5c4f74c5526a5da88790fef387aa8b8213dabf842200"},{"module":"Relation.Binary.PropositionalEquality.Properties","origin":"library","sha256":"4ed071c430e9244d3be9b9ca847d74232826c0fed7bf3035da0a6d4a8c7b2137"},{"module":"Relation.Binary.Reasoning.Syntax","origin":"library","sha256":"a7a831d62ed2a3c7d5d0f29521162fbf264d34a48b6c91e9ac9f6168c2067ceb"},{"module":"Relation.Binary.Structures","origin":"library","sha256":"12ccbc4bd7da510ed8edf17018eb10b3d827e08ba1842a623c3370c2cb6ef396"},{"module":"Relation.Nullary","origin":"library","sha256":"56f7f4a54b8d655b0c90dacfd65d29cfc2d7e73d8666bd30a934ae25818a5019"},{"module":"Relation.Nullary.Decidable.Core","origin":"library","sha256":"0082f72e3d2bd247d56d46abf3f70936a08d32c69c3a18cb68f744c8fefb67b8"},{"module":"Relation.Nullary.Negation.Core","origin":"library","sha256":"b848e89c226674f8462c9c5aced87e5aa3fe03fdf9cbaffd0c28e9f87ff6c910"},{"module":"Relation.Nullary.Recomputable","origin":"library","sha256":"cacf1a1d98ceed1571bac2ca9a3c1f9967ea6c91fd0dc0ed35b5fc74657b7ce0"},{"module":"Relation.Nullary.Reflects","origin":"library","sha256":"73ec20b5e43a3903b68b994cd0815b9d0c3dcc9e57dae39b4d8b487904a7eea1"},{"module":"Relation.Unary","origin":"library","sha256":"4960f1b9004f19834cbc0271b80a64281a99ba715ffa125f73df80f205745a71"}]},"kind":"agda-cone-receipt","policy":"standards 3-practice/PROOF-POLICY.adoc §8.2, §8.4","postulate_scan":{"findings":[],"kernel_primitives":[{"line":26,"module":"Agda.Primitive","text":"postulate"},{"line":34,"module":"Agda.Primitive","text":"postulate"}],"method":"comment-aware: nested block and line comments removed, pragmas kept; string literals not lexed","result":"clean"},"schema_version":1,"source":{"commit":"22f6f723fce6e7ae1a1f145b7954f731aa12a033","entrypoint":"Burrow/Trust.agda","repository":"https://github.com/hyperpolymath/proof-burrower","uncommitted_changes_under_entry_dir":false},"toolchain":{"agda":"Agda version 2.7.0.1","agda_executable_sha256":"6de41437c14c05c9fe576d724cc67386444c0fa9fee662a08250fefb91bee8b6","flags":["--safe","--without-K","--cubical-compatible"],"stdlib_archive_sha256":"72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431"}}
+{"import_cone":{"count":35,"modules":[{"module":"Agda.Builtin.Bool","origin":"agda-kernel","sha256":"514fa25a0df7064cdb213507a0f6332c97288a52d538be3a9df06cc7001ba7f5"},{"module":"Agda.Builtin.Equality","origin":"agda-kernel","sha256":"5735edb0be7e530133814e9431d1466bb1e7892c2a4746c1a0d2a3a0dbea91cd"},{"module":"Agda.Builtin.Maybe","origin":"agda-kernel","sha256":"982f7f2afbfbc4ac41b6bdafddfb5e032a5ddfa71e204f39bbecc23967dc4808"},{"module":"Agda.Builtin.Sigma","origin":"agda-kernel","sha256":"5c393f230b359032f64ff78ad693799a162dbf9cada2089048aedb4c6f669e1f"},{"module":"Agda.Builtin.Unit","origin":"agda-kernel","sha256":"03d06283f9d8005beff99fd42de38b7315aa7697099ea22fc19d060600b16249"},{"module":"Agda.Primitive","origin":"agda-kernel","sha256":"e5e4e04900cf1a28202e2ff26bb20d6fa6401fcc9f4049cd8d14fedd5bd697f8"},{"module":"Burrow.Ledger","origin":"first-party","sha256":"eaf110f4f0b97fe0ba6d74f21f65881241600ce8299288fe47ba10e6ff45ae64"},{"module":"Burrow.Trust","origin":"first-party","sha256":"5ba1de66b2e4845b7d3663bba338481697e87712cf32da3bb55816da775cce06"},{"module":"Data.Bool.Base","origin":"library","sha256":"124e425ebafee9cbe8fb496b4c8467fdd372b0961ca03e445bfda506738204f6"},{"module":"Data.Empty","origin":"library","sha256":"3a68a9e529c13054202a3892bfcf961bb75db2dc11d63f068189c4cbd48c2cd2"},{"module":"Data.Irrelevant","origin":"library","sha256":"5f225770f471847144eb3908fecb1d4b0a06e7d7b1cb3a12bdebd840bf17a783"},{"module":"Data.Product.Base","origin":"library","sha256":"e2585b0cc6d0c2486cf1f30bd98a3855b00666e8aa8bc0aee5be8253c952a99c"},{"module":"Data.Sum.Base","origin":"library","sha256":"2733ba66eaed94cc0f0b21f2a9ed0533f8a31b5bd487e40384632f1d6204fcfd"},{"module":"Data.Unit","origin":"library","sha256":"320fc4c784fbb6ad847f41ae317f60da346002a119cbca178b2caaa787c2b26c"},{"module":"Data.Unit.Base","origin":"library","sha256":"38cc799f18b6f106336ace8ae66c5a171251c0eb3b6bf32124e33c45d441b2fb"},{"module":"Data.Unit.Polymorphic.Base","origin":"library","sha256":"002ae814be1dafd6f6c4193a2254ee19f7793ffef7dcf1d29f9794db0b19f2a8"},{"module":"Data.Unit.Properties","origin":"library","sha256":"bb9a390596f27739aa9d9c46ef666e42917df4f5000f675ef1042abe3fe2fc62"},{"module":"Function.Base","origin":"library","sha256":"b021bf843c1974a5d50a1a3362f2d6447018629331a3dc2bb0d9ea85ec029e84"},{"module":"Level","origin":"library","sha256":"1168f8373370c10aec0f20bae0cc43db9a34331a49deb4c72efd2574a638a278"},{"module":"Relation.Binary.Bundles","origin":"library","sha256":"fd4b0a832bf9f372d2739668c7e0988e0242519686b69616dc67043923ad88c3"},{"module":"Relation.Binary.Consequences","origin":"library","sha256":"d5f1d178492b9e485a3efdcb16dd18fe623896371e2cae3662d8fde1ff94a455"},{"module":"Relation.Binary.Construct.Composition","origin":"library","sha256":"829ca14501f085b08a0504a61c7874cd20cce07ffc883027ef3465e4f44cf347"},{"module":"Relation.Binary.Core","origin":"library","sha256":"09eda35f4c2f795542f0a2468ade41793e9c9e07889553989e03d343902fcb81"},{"module":"Relation.Binary.Definitions","origin":"library","sha256":"c61495efb42702588229a67461c451dd660bd5d686c244ee1895b9d563547783"},{"module":"Relation.Binary.Properties.Setoid","origin":"library","sha256":"ba05a90fbede6b120c7aefe56944f0c5c772f908a1f60d1644ec4c70c9a93293"},{"module":"Relation.Binary.PropositionalEquality.Core","origin":"library","sha256":"480da0675a0d8ddddcae5c4f74c5526a5da88790fef387aa8b8213dabf842200"},{"module":"Relation.Binary.PropositionalEquality.Properties","origin":"library","sha256":"4ed071c430e9244d3be9b9ca847d74232826c0fed7bf3035da0a6d4a8c7b2137"},{"module":"Relation.Binary.Reasoning.Syntax","origin":"library","sha256":"a7a831d62ed2a3c7d5d0f29521162fbf264d34a48b6c91e9ac9f6168c2067ceb"},{"module":"Relation.Binary.Structures","origin":"library","sha256":"12ccbc4bd7da510ed8edf17018eb10b3d827e08ba1842a623c3370c2cb6ef396"},{"module":"Relation.Nullary","origin":"library","sha256":"56f7f4a54b8d655b0c90dacfd65d29cfc2d7e73d8666bd30a934ae25818a5019"},{"module":"Relation.Nullary.Decidable.Core","origin":"library","sha256":"0082f72e3d2bd247d56d46abf3f70936a08d32c69c3a18cb68f744c8fefb67b8"},{"module":"Relation.Nullary.Negation.Core","origin":"library","sha256":"b848e89c226674f8462c9c5aced87e5aa3fe03fdf9cbaffd0c28e9f87ff6c910"},{"module":"Relation.Nullary.Recomputable","origin":"library","sha256":"cacf1a1d98ceed1571bac2ca9a3c1f9967ea6c91fd0dc0ed35b5fc74657b7ce0"},{"module":"Relation.Nullary.Reflects","origin":"library","sha256":"73ec20b5e43a3903b68b994cd0815b9d0c3dcc9e57dae39b4d8b487904a7eea1"},{"module":"Relation.Unary","origin":"library","sha256":"4960f1b9004f19834cbc0271b80a64281a99ba715ffa125f73df80f205745a71"}]},"kind":"agda-cone-receipt","policy":"standards 3-practice/PROOF-POLICY.adoc §8.2, §8.4","postulate_scan":{"findings":[],"kernel_primitives":[{"line":26,"module":"Agda.Primitive","text":"postulate"},{"line":34,"module":"Agda.Primitive","text":"postulate"}],"method":"comment-aware: nested block and line comments removed, pragmas kept; string literals not lexed","result":"clean"},"schema_version":1,"source":{"commit":"22f6f723fce6e7ae1a1f145b7954f731aa12a033","entrypoint":"Burrow/Ledger.agda","repository":"https://github.com/hyperpolymath/proof-burrower","uncommitted_changes_under_entry_dir":false},"toolchain":{"agda":"Agda version 2.7.0.1","agda_executable_sha256":"6de41437c14c05c9fe576d724cc67386444c0fa9fee662a08250fefb91bee8b6","flags":["--safe","--without-K","--cubical-compatible"],"stdlib_archive_sha256":"72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431"}}
diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc
index 0e51571..b9a3b05 100644
--- a/docs/status/PROOF-STATUS.adoc
+++ b/docs/status/PROOF-STATUS.adoc
@@ -17,10 +17,24 @@
 
 *Overall*: 2 of 14 tracked obligations proven.
 
-Estate grade (`hyperpolymath/mathesis` §5): the two Domain proofs are
-*Grade 3* — constructed in Agda and type-checked locally, not yet
-translated to an independent foundational system. Nothing else in this
-repository has a grade.
+Estate grade: the only proof grade is the *Proof Witness Grade* (PWG) of
+standards `3-practice/PROOF-POLICY.adoc` §8, which supersedes the Mathesis
+brief's "Grade 3" wording. A grade is derived from receipts, never asserted.
+DOM-1 and DOM-2 are theory. Census, by obligation: `PWG-1` 0/2,
+`PWG-2ii` 0/2, `PWG-2i` 0/2, `PWG-3` 2/2, ungraded 0/2; neither carries
+`+foundation-diverse`.
+
+`PWG-3` is derived from the receipts in
+`docs/reports/2026-11-09-agda-cone-receipts.jsonl` (§8.2, §8.4), written by
+`scripts/ci/agda-cone-receipt.sh` at `22f6f723` with no uncommitted change
+under `verification/proofs/agda/`: Agda 2.7.0.1 (the pinned release),
+agda-stdlib 2.1 (archive SHA-256 `72ca3ea2…`), flags
+`--safe --without-K --cubical-compatible`, import cones of 34 modules
+(`Burrow.Trust`) and 35 (`Burrow.Ledger`) with a digest per file, and a
+clean comment-aware postulate scan (the only postulates are Agda.Primitive's
+universe-level primitives). The `agda` job in `proof-safety.yml` re-checks
+both modules and writes the same receipts on every run. Neither result has
+a Rocq or Lean recheck leg, so neither can rise above `PWG-3` yet.
 
 === Proofs Done
 
@@ -33,19 +47,32 @@ repository has a grade.
  Kripke countermodel shows the legacy marker has no soundness witness
  |Agda 2.7.0.1
 |`verification/proofs/agda/Burrow/Trust.agda`
-|2026-11-01
-|`just proof-check-agda`, `agda --safe --without-K --cubical-compatible`,
- 0 warnings; also clean under full `--cubical`
+|2026-11-03 (#119)
+|CI `proof-safety.yml` job `agda` (pinned Agda 2.7.0.1, stdlib 2.1) and
+ receipt `docs/reports/2026-11-09-agda-cone-receipts.jsonl`; 0 warnings;
+ also clean under full `--cubical`
 
 |DOM-2
 |Ledger read path: no function from a stored record to the fact exists
  (`no-launder`); promotion needs a per-record soundness witness
  |Agda 2.7.0.1
 |`verification/proofs/agda/Burrow/Ledger.agda`
-|2026-11-01
+|2026-11-03 (#119)
 |As DOM-1
 |===
 
+*Scope, from the 2026-11-09 audit.* DOM-2 is a *specification*: the Rust
+`Ledger::read_all` (`crates/burrower-core/src/ledger.rs`) does not yet
+re-validate `extra.receipt` on read, so the read rule is not a property of
+the code. That Rust obligation belongs to Creusot/Pearlite and Verus
+(PROOF-POLICY §1.2) and is not yet tracked as a row. `no-launder` and
+`no-legacy-soundness` amount to "no map from inhabited evidence to ⊥" and do
+not need the Kripke model; `epi-is-not-factive` was the identity function on
+`¬ X` and has been restated as `¬ (∀ {A} → Epi A → A)`, proved from the
+legacy countermodel. `revalidate` and `promote` had implicit arguments no use
+site could infer; `revalidate` drops the unused one and `promote` takes its
+record explicitly.
+
 These two are the semantic record that was missing: before 2026-11-01 the
 receipt/warrant distinction existed only as a Rust `Option<ProofReceipt>`
 and a sentence in the ledger explanation, so nothing pinned down which
@@ -122,7 +149,13 @@ panic-attack assail --proofs-only
 |===
 |Date |Change |By
 |2026-04-04 |Initial proof status tracking |Template
-|2026-11-01 |DOM-1 and DOM-2 proved in Agda (Grade 3); DOM-3..7 added;
+|2026-11-01 |DOM-1 and DOM-2 proved in Agda; DOM-3..7 added;
  `just proof-check-agda` moved to the estate canonical flags with an
  include path |Audit 2026-11-01
+|2026-11-09 |Grades restated as PROOF-POLICY §8 PWG and derived from
+ committed cone receipts (`PWG-3` 2/2); CI `agda` job with pinned
+ toolchain; `epi-is-not-factive` restated; `revalidate`/`promote`
+ made usable; wrapper fixed for hierarchical modules; proof recipes fail
+ when a prover is missing; dangerous-pattern scan ignores comments
+ |Proof audit 2026-11-09
 |===
diff --git a/scripts/agda-safe-check.sh b/scripts/agda-safe-check.sh
index eac4b04..1f7bc07 100644
--- a/scripts/agda-safe-check.sh
+++ b/scripts/agda-safe-check.sh
@@ -18,22 +18,46 @@ if [[ "$checker" != /* ]]; then
 fi
 "$checker" --version >&2
 include_args=()
+# The pinned toolchain (scripts/ci/setup-agda.sh) names its libraries file in
+# AGDA_LIBRARIES_FILE. Agda reads no such variable, only --library-file, so
+# without this a root carrying an .agda-lib (burrow.agda-lib depends on
+# standard-library-2.1) resolves against ~/.config/agda/libraries instead.
+if [[ -n "${AGDA_LIBRARIES_FILE:-}" ]]; then
+  if [[ ! -f "$AGDA_LIBRARIES_FILE" ]]; then
+    echo "Agda libraries file unavailable: $AGDA_LIBRARIES_FILE" >&2
+    exit 2
+  fi
+  include_args=(--no-default-libraries --library-file "$(realpath -e -- "$AGDA_LIBRARIES_FILE")")
+fi
 if [[ -n "${AGDA_LIBRARY_INCLUDE:-}" ]]; then
   if [[ ! -d "$AGDA_LIBRARY_INCLUDE" ]]; then
     echo "Agda library source directory unavailable: $AGDA_LIBRARY_INCLUDE" >&2
     exit 2
   fi
-  include_args=(-i "$(realpath -e -- "$AGDA_LIBRARY_INCLUDE")")
+  include_args+=(-i "$(realpath -e -- "$AGDA_LIBRARY_INCLUDE")")
 fi
 for source in "$@"; do
   if [[ "$source" == -* || "$source" != *.agda || ! -f "$source" ]]; then
     echo "Not a readable Agda source (options forbidden): $source" >&2
     exit 2
   fi
-  module="$(realpath -e -- "$source")"
-  # Module Properties in path/to/Properties.agda must be checked from
-  # path/to, rather than forcing a false module/path mismatch at repo root.
-  ( cd -- "$(dirname -- "$module")" &&
+  file="$(realpath -e -- "$source")"
+  # Agda checks a module from its include root: module Burrow.Trust in
+  # path/to/Burrow/Trust.agda is checked from path/to as Burrow/Trust.agda.
+  # Read the module name from the file and walk up one directory per
+  # component, so hierarchical modules work as well as flat ones.
+  name="$(sed -nE 's/^[[:space:]]*module[[:space:]]+([A-Za-z0-9_.]+)[[:space:]].*/\1/p' "$file" | head -n 1)"
+  if [[ -z "$name" ]]; then
+    echo "No module declaration in $source" >&2
+    exit 2
+  fi
+  rel="${name//.//}.agda"
+  root="${file%/"$rel"}"
+  if [[ "$root" == "$file" || "$root/$rel" != "$file" ]]; then
+    echo "Module $name does not match its path $source" >&2
+    exit 2
+  fi
+  ( cd -- "$root" &&
     "$checker" --safe --without-K --cubical-compatible \
-      "${include_args[@]}" "$(basename -- "$module")" )
+      "${include_args[@]}" "$rel" )
 done
diff --git a/scripts/ci/agda-cone-receipt.sh b/scripts/ci/agda-cone-receipt.sh
new file mode 100755
index 0000000..1465e09
--- /dev/null
+++ b/scripts/ci/agda-cone-receipt.sh
@@ -0,0 +1,138 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell
+#
+# agda-cone-receipt.sh ENTRY.agda — the PROOF-POLICY §8.2 receipt for the
+# theory theorems in ENTRY: the Agda version, the standard-library pin, the
+# flags in force, the import cone with a SHA-256 per file, and a
+# comment-aware scan of that cone for postulates, unsafe pragmas and
+# primTrustMe (§8.4). Writes one JCS object to stdout.
+#
+# Run from the Agda include root after the type check, in the environment
+# scripts/ci/setup-agda.sh prepares (AGDA_LIBRARIES_FILE, Agda_datadir).
+# AGDA_STDLIB_SHA256 names the pinned stdlib archive digest.
+#
+# The scan reads Agda source with nested {- -} block comments and -- line
+# comments removed and {-# #-} pragmas kept. It does not lex string
+# literals; a literal holding "{-" would hide text from it, and --safe is
+# still the check that refuses escape hatches. The scan is the record §8.4
+# asks for, not a replacement for --safe.
+#
+# Postulates in the Agda data directory (Agda.Primitive's universe-level
+# primitives) belong to the Agda kernel's trust base. They are listed in the
+# receipt, not counted as findings.
+#
+# Exit codes: 0 receipt written and the scan is clean, 1 a finding outside
+# the kernel's own primitives, 2 cannot run.
+set -euo pipefail
+export LC_ALL=C.UTF-8
+
+# strip <file>: source with comments removed and pragmas kept.
+strip() {
+  awk '
+    { line = $0; out = ""; i = 1; n = length(line)
+      while (i <= n) {
+        two = substr(line, i, 2); three = substr(line, i, 3)
+        if (depth == 0 && inpragma == 0 && three == "{-#") { inpragma = 1; out = out three; i += 3; continue }
+        if (inpragma == 1 && three == "#-}") { inpragma = 0; out = out three; i += 3; continue }
+        if (inpragma == 1) { out = out substr(line, i, 1); i++; continue }
+        if (depth == 0 && two == "--") break
+        if (two == "{-") { depth++; i += 2; continue }
+        if (depth > 0 && two == "-}") { depth--; i += 2; continue }
+        if (depth == 0) out = out substr(line, i, 1)
+        i++
+      }
+      print out }' "$1"
+}
+
+# scan: the escape hatches the receipt records, one "line:text" per hit.
+scan() {
+  { strip "$1" | grep -nE '(^|[[:space:](){};])postulate($|[[:space:](){};])|\{-#[[:space:]]*(TERMINATING|NON_TERMINATING|NO_POSITIVITY_CHECK|NO_UNIVERSE_CHECK|NON_COVERING)|primTrustMe' || true; }
+}
+
+# Sourced by scripts/ci/test-agda-cone-receipt.sh for strip and scan only.
+# shellcheck disable=SC2317 # exit runs only when executed rather than sourced
+if [[ "${AGDA_CONE_RECEIPT_FUNCTIONS_ONLY:-}" == 1 ]]; then return 0 2>/dev/null || exit 0; fi
+
+entry=${1:?usage: agda-cone-receipt.sh ENTRY.agda}
+flags=(--safe --without-K --cubical-compatible)
+if ! command -v agda >/dev/null 2>&1 || [[ ! -f "${AGDA_LIBRARIES_FILE:-}" ]]; then
+  echo "agda-cone-receipt: pinned Agda setup missing" >&2; exit 2
+fi
+command -v jq >/dev/null 2>&1 || { echo "agda-cone-receipt: jq missing" >&2; exit 2; }
+
+tmp=$(mktemp -d)
+trap 'rm -rf "$tmp"' EXIT
+
+agda --no-default-libraries --library-file "$AGDA_LIBRARIES_FILE" "${flags[@]}" \
+  --dependency-graph="$tmp/cone.dot" "$entry" > "$tmp/agda.log" 2>&1 \
+  || { cat "$tmp/agda.log" >&2; echo "agda-cone-receipt: agda failed" >&2; exit 2; }
+
+data_dir=$(agda --print-agda-data-dir)
+# Include roots: the Agda data directory's lib/prim, then every library's
+# include directories from the library file (one .agda-lib path per line).
+roots=("$data_dir/lib/prim")
+while IFS= read -r lib; do
+  [[ -n "$lib" ]] || continue
+  libdir=$(dirname -- "$lib")
+  while IFS= read -r inc; do
+    roots+=("$libdir/$inc")
+  done < <(awk '/^include:/ { sub(/^include:[[:space:]]*/, ""); n = split($0, a, /[[:space:]]+/); for (i = 1; i <= n; i++) if (a[i] != "") print a[i] }' "$lib")
+done < "$AGDA_LIBRARIES_FILE"
+
+# Module names from the dot file's node labels.
+grep -oE 'label="[^"]+"' "$tmp/cone.dot" | sed -E 's/^label="//; s/"$//' | sort -u > "$tmp/modules"
+[[ -s "$tmp/modules" ]] || { echo "agda-cone-receipt: empty dependency graph" >&2; exit 2; }
+
+: > "$tmp/cone.jsonl"; : > "$tmp/findings.jsonl"; : > "$tmp/kernel.jsonl"
+while IFS= read -r module; do
+  rel="${module//.//}"
+  file=""
+  for root in "${roots[@]}"; do
+    for ext in agda lagda lagda.md; do
+      [[ -f "$root/$rel.$ext" ]] && { file="$root/$rel.$ext"; break 2; }
+    done
+  done
+  [[ -n "$file" ]] || { echo "agda-cone-receipt: cannot locate module $module" >&2; exit 2; }
+  file=$(realpath -- "$file")
+  case "$file" in
+    "$(realpath -- "$data_dir")"/*) origin=agda-kernel ;;
+    "$(realpath -- "$PWD")"/*) origin=first-party ;;
+    *) origin=library ;;
+  esac
+  digest=$(sha256sum "$file" | cut -d' ' -f1)
+  jq -cn --arg m "$module" --arg o "$origin" --arg d "$digest" '{module: $m, origin: $o, sha256: $d}' >> "$tmp/cone.jsonl"
+  scan "$file" \
+    | while IFS=: read -r ln text; do
+        if [[ "$origin" == agda-kernel ]]; then target="$tmp/kernel.jsonl"; else target="$tmp/findings.jsonl"; fi
+        jq -cn --arg m "$module" --argjson l "$ln" --arg t "$text" '{module: $m, line: $l, text: ($t | gsub("^\\s+|\\s+$"; ""))}' >> "$target"
+      done
+done < "$tmp/modules"
+
+commit=$(git rev-parse HEAD)
+dirty=$(git status --porcelain -- . | head -1)
+agda_bin=$(command -v agda)
+jq -cnS \
+  --arg commit "$commit" --arg dirty "${dirty:+yes}" --arg entry "$entry" \
+  --arg agda "$(agda --version)" --arg agda_sha "$(sha256sum "$agda_bin" | cut -d' ' -f1)" \
+  --arg stdlib_sha "${AGDA_STDLIB_SHA256:-unrecorded}" \
+  --argjson flags "$(printf '%s\n' "${flags[@]}" | jq -R . | jq -s .)" \
+  --slurpfile cone "$tmp/cone.jsonl" --slurpfile findings "$tmp/findings.jsonl" \
+  --slurpfile kernel "$tmp/kernel.jsonl" '
+  {
+    schema_version: 1,
+    kind: "agda-cone-receipt",
+    policy: "standards 3-practice/PROOF-POLICY.adoc §8.2, §8.4",
+    source: {repository: "https://github.com/hyperpolymath/proof-burrower", commit: $commit,
+             uncommitted_changes_under_entry_dir: ($dirty == "yes"), entrypoint: $entry},
+    toolchain: {agda: $agda, agda_executable_sha256: $agda_sha,
+                stdlib_archive_sha256: $stdlib_sha, flags: $flags},
+    import_cone: {count: ($cone | length), modules: $cone},
+    postulate_scan: {
+      method: "comment-aware: nested block and line comments removed, pragmas kept; string literals not lexed",
+      kernel_primitives: $kernel,
+      findings: $findings,
+      result: (if ($findings | length) == 0 then "clean" else "findings" end)
+    }
+  }'
+[[ ! -s "$tmp/findings.jsonl" ]]
diff --git a/scripts/ci/setup-agda.sh b/scripts/ci/setup-agda.sh
new file mode 100755
index 0000000..0a4b6f4
--- /dev/null
+++ b/scripts/ci/setup-agda.sh
@@ -0,0 +1,62 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell
+# Pinned upstream binaries: no cold GHC bootstrap and no cached proof results.
+set -Eeuo pipefail
+trap 'echo "::error::Agda setup did not complete; proof check NOT RUN"; exit 2' ERR
+
+if [[ "$(uname -s)" != Linux || "$(uname -m)" != x86_64 ]]; then
+  echo "::error::The pinned Agda distribution supports Linux x86_64; proof check NOT RUN"
+  exit 2
+fi
+
+agda_version=2.7.0.1
+stdlib_version=2.1
+cache_dir="${AGDA_ARCHIVE_CACHE:-${HOME}/.cache/echidna/agda}"
+mkdir -p "$cache_dir"
+toolchain_dir=$(mktemp -d "${RUNNER_TEMP:-${TMPDIR:-/tmp}}/echidna-agda.XXXXXX")
+repo_root=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")/../.." && pwd)
+
+fetch_verified() {
+  local url=$1 archive=$2 digest=$3
+  if [[ -f "$archive" ]] && ! printf '%s  %s\n' "$digest" "$archive" | sha256sum --check --status; then
+    echo "::warning::Discarding a corrupt cached archive: ${archive##*/}"
+    rm -- "$archive"
+  fi
+  if [[ ! -f "$archive" ]]; then
+    curl --fail --location --retry 3 --output "$archive.download" "$url"
+    printf '%s  %s\n' "$digest" "$archive.download" | sha256sum --check
+    mv -- "$archive.download" "$archive"
+  fi
+  # Recheck warm restores too: a cache hit alone never authenticates a compiler.
+  printf '%s  %s\n' "$digest" "$archive" | sha256sum --check
+}
+
+agda_archive="$cache_dir/Agda-v${agda_version}-linux.tar.xz"
+stdlib_archive="$cache_dir/agda-stdlib-${stdlib_version}.tar.gz"
+fetch_verified \
+  "https://github.com/agda/agda/releases/download/v${agda_version}/Agda-v${agda_version}-linux.tar.xz" \
+  "$agda_archive" 975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a
+fetch_verified \
+  "https://github.com/agda/agda-stdlib/archive/refs/tags/v${stdlib_version}.tar.gz" \
+  "$stdlib_archive" 72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431
+
+tar --no-same-owner -xJf "$agda_archive" -C "$toolchain_dir"
+tar --no-same-owner -xzf "$stdlib_archive" -C "$toolchain_dir"
+agda_dir="$toolchain_dir/Agda-v${agda_version}"
+libraries="$toolchain_dir/libraries"
+printf '%s\n' \
+  "$toolchain_dir/agda-stdlib-${stdlib_version}/standard-library.agda-lib" \
+  "$repo_root/verification/proofs/agda/burrow.agda-lib" > "$libraries"
+"$agda_dir/bin/agda" --version
+
+if [[ -n "${GITHUB_ENV:-}" && -n "${GITHUB_PATH:-}" ]]; then
+  {
+    printf 'Agda_datadir=%s\n' "$agda_dir/data"
+    printf 'AGDA_LIBRARIES_FILE=%s\n' "$libraries"
+    printf 'LC_ALL=C.UTF-8\n'
+  } >> "$GITHUB_ENV"
+  printf '%s\n' "$agda_dir/bin" >> "$GITHUB_PATH"
+fi
+printf 'Agda data: %s\nLibraries: %s\nExecutable: %s\n' \
+  "$agda_dir/data" "$libraries" "$agda_dir/bin/agda"
diff --git a/scripts/ci/test-agda-cone-receipt.sh b/scripts/ci/test-agda-cone-receipt.sh
new file mode 100755
index 0000000..4998508
--- /dev/null
+++ b/scripts/ci/test-agda-cone-receipt.sh
@@ -0,0 +1,32 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell
+# Fixture test for the comment-aware scan in agda-cone-receipt.sh: comments
+# (line, block, nested) hide nothing they should not, pragmas stay visible,
+# and only the keyword `postulate` counts, not identifiers that contain it.
+set -euo pipefail
+here=$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd)
+# shellcheck source=scripts/ci/agda-cone-receipt.sh
+AGDA_CONE_RECEIPT_FUNCTIONS_ONLY=1 . "$here/agda-cone-receipt.sh"
+tmp=$(mktemp -d)
+trap 'rm -rf "$tmp"' EXIT
+cat > "$tmp/Fx.agda" <<'AGDA'
+module Fx where
+-- postulate in a line comment
+{- postulate in a block {- nested postulate -} still comment postulate -}
+x = 1 -- trailing postulate
+{-# TERMINATING #-}
+postulate
+  ax : Set
+postulates-name : Set
+f = primTrustMe
+{-# OPTIONS --safe #-}
+AGDA
+got=$(scan "$tmp/Fx.agda" | cut -d: -f1 | tr '\n' ' ')
+want="5 6 9 "
+if [[ "$got" == "$want" ]]; then
+  echo "agda-cone-receipt scan: ok (hits on lines $got)"
+else
+  echo "::error::agda-cone-receipt scan: hits on lines '$got', want '$want'"
+  exit 1
+fi
diff --git a/scripts/proof-scan-dangerous.sh b/scripts/proof-scan-dangerous.sh
new file mode 100755
index 0000000..cc00283
--- /dev/null
+++ b/scripts/proof-scan-dangerous.sh
@@ -0,0 +1,51 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Scan first-party proof sources for escape hatches, ignoring comments.
+#
+# The old grep matched header comments ("no postulate here") and failed on
+# main with eight false positives, which drowned any real hit. Comments are
+# removed per language before matching; Agda/Idris/Lean pragmas are kept.
+#   Agda, Idris 2   -- line, {- -} block (nested), {-# pragma #-} kept
+#   Lean 4          -- line, /- -/ block (nested)
+#   Rocq/Coq        (* *) block (nested)
+# String literals are not lexed. Usage: proof-scan-dangerous.sh [DIR]
+set -euo pipefail
+dir="${1:-verification/proofs}"
+patterns='(^|[^A-Za-z0-9_-])(believe_me|assert_total|postulate|sorry|Admitted|admit|unsafeCoerce|Obj\.magic|primTrustMe)([^A-Za-z0-9_-]|$)|\{-#[[:space:]]*(TERMINATING|NON_TERMINATING|NO_POSITIVITY_CHECK|NON_COVERING)'
+
+# strip FILE OPEN CLOSE LINE: comments removed; LINE empty when none.
+strip() {
+  awk -v op="$2" -v cl="$3" -v ln_c="$4" '
+    { s = $0; out = ""; i = 1; n = length(s)
+      while (i <= n) {
+        if (depth == 0 && op == "{-" && substr(s, i, 3) == "{-#") { prag = 1 }
+        if (prag) { out = out substr(s, i, 1); if (substr(s, i, 3) == "#-}") { out = out "-}"; i += 3; prag = 0; continue } i++; continue }
+        if (depth == 0 && ln_c != "" && substr(s, i, length(ln_c)) == ln_c) break
+        if (substr(s, i, length(op)) == op) { depth++; i += length(op); continue }
+        if (depth > 0 && substr(s, i, length(cl)) == cl) { depth--; i += length(cl); continue }
+        if (depth == 0) out = out substr(s, i, 1)
+        i++
+      }
+      print out }' "$1"
+}
+
+found=0
+while IFS= read -r -d '' f; do
+  case "$f" in
+    *.agda|*.idr) text=$(strip "$f" '{-' '-}' '--') ;;
+    *.lean)       text=$(strip "$f" '/-' '-/' '--') ;;
+    *.v)          text=$(strip "$f" '(*' '*)' '') ;;
+    *) continue ;;
+  esac
+  hits=$(grep -nE "$patterns" <<<"$text" || true)
+  if [[ -n "$hits" ]]; then
+    echo "  DANGEROUS: $f"
+    while IFS= read -r h; do echo "    $h"; done <<<"$hits"
+    found=$((found + 1))
+  fi
+done < <(find "$dir" -type f \( -name '*.agda' -o -name '*.idr' -o -name '*.lean' -o -name '*.v' \) -print0 | sort -z)
+if [[ "$found" -gt 0 ]]; then
+  echo "FAIL: $found file(s) contain escape hatches outside comments"
+  exit 1
+fi
+echo "PASS: no escape hatches outside comments"
diff --git a/tests/agda-safe-check.sh b/tests/agda-safe-check.sh
index 98ecce0..2d23050 100644
--- a/tests/agda-safe-check.sh
+++ b/tests/agda-safe-check.sh
@@ -3,6 +3,8 @@
 # Tests scripts/agda-safe-check.sh with a fake Agda executable.
 # Checks the canonical safe Agda options, rejection of --with-K, and failure when the checker is missing.
 set -euo pipefail
+# The pinned-toolchain variables must not leak in from a CI job environment.
+unset AGDA_LIBRARIES_FILE AGDA_LIBRARY_INCLUDE
 root="$(cd "$(dirname "$0")/.." && pwd)"
 tmp="$(mktemp -d)"
 trap 'rm -rf "$tmp"' EXIT
@@ -26,6 +28,20 @@ mapfile -t args < "$tmp/capture"
 [[ "${args[1]}" == --without-K && "${args[2]}" == --cubical-compatible ]]
 [[ "${args[3]}" == Test.agda ]]
 [[ "$(cat "$tmp/cwd")" == "$tmp/nested" ]]
+# A hierarchical module is checked from its include root (audit 2026-11-09:
+# the wrapper used to cd into Burrow/ and fail on Burrow.Trust).
+mkdir -p "$tmp/root/Burrow"
+printf 'module Burrow.Trust where\n' > "$tmp/root/Burrow/Trust.agda"
+AGDA_BIN="$tmp/fake-agda" AGDA_CAPTURE="$tmp/capture" \
+ AGDA_CWD_CAPTURE="$tmp/cwd" bash "$root/scripts/agda-safe-check.sh" "$tmp/root/Burrow/Trust.agda"
+mapfile -t args < "$tmp/capture"
+[[ "${args[3]}" == Burrow/Trust.agda && "$(cat "$tmp/cwd")" == "$tmp/root" ]]
+# A module whose name does not match its path is refused.
+printf 'module Elsewhere where\n' > "$tmp/root/Burrow/Wrong.agda"
+if AGDA_BIN="$tmp/fake-agda" AGDA_CAPTURE="$tmp/capture" AGDA_CWD_CAPTURE="$tmp/cwd" \
+  bash "$root/scripts/agda-safe-check.sh" "$tmp/root/Burrow/Wrong.agda" 2>/dev/null; then
+  echo "a module/path mismatch was accepted" >&2; exit 1
+fi
 AGDA_BIN="$tmp/fake-agda" AGDA_CAPTURE="$tmp/capture" AGDA_CWD_CAPTURE="$tmp/cwd" \
  AGDA_LIBRARY_INCLUDE="$tmp/stdlib" bash "$root/scripts/agda-safe-check.sh" "$tmp/nested/Test.agda"
 mapfile -t args < "$tmp/capture"
@@ -42,4 +58,18 @@ if AGDA_BIN="$tmp/fake-agda" AGDA_LIBRARY_INCLUDE="$tmp/missing" \
   bash "$root/scripts/agda-safe-check.sh" "$tmp/nested/Test.agda"; then
   echo "missing include directory was accepted" >&2; exit 1
 fi
-echo 'Agda safe invocation, nested module, include path, and negative controls passed'
+# The pinned libraries file reaches Agda as --library-file (Agda reads no
+# AGDA_LIBRARIES_FILE variable), ahead of any -i include.
+printf "%s\n" "$tmp/stdlib/standard-library.agda-lib" > "$tmp/libraries"
+AGDA_BIN="$tmp/fake-agda" AGDA_CAPTURE="$tmp/capture" AGDA_CWD_CAPTURE="$tmp/cwd" \
+ AGDA_LIBRARIES_FILE="$tmp/libraries" AGDA_LIBRARY_INCLUDE="$tmp/stdlib" \
+ bash "$root/scripts/agda-safe-check.sh" "$tmp/nested/Test.agda"
+mapfile -t args < "$tmp/capture"
+[[ "${#args[@]}" -eq 9 && "${args[3]}" == --no-default-libraries ]]
+[[ "${args[4]}" == --library-file && "${args[5]}" == "$tmp/libraries" ]]
+[[ "${args[6]}" == -i && "${args[7]}" == "$tmp/stdlib" && "${args[8]}" == Test.agda ]]
+if AGDA_BIN="$tmp/fake-agda" AGDA_LIBRARIES_FILE="$tmp/no-such-libraries" \
+  bash "$root/scripts/agda-safe-check.sh" "$tmp/nested/Test.agda"; then
+  echo "missing libraries file was accepted" >&2; exit 1
+fi
+echo "Agda safe invocation, nested module, include path, libraries file, and negative controls passed"
diff --git a/verification/proofs/agda/Burrow/Ledger.agda b/verification/proofs/agda/Burrow/Ledger.agda
index c4fa422..3e252d9 100644
--- a/verification/proofs/agda/Burrow/Ledger.agda
+++ b/verification/proofs/agda/Burrow/Ledger.agda
@@ -59,11 +59,13 @@ read (storedClaim w t) = epi w t
 -- Promotion is not a property of the record.  It needs a witness for that
 -- record's warrant, supplied by the reader — i.e. by re-running the
 -- validation against what is actually stored.
+-- The record is explicit: a projection cannot be inverted, so Agda could
+-- never infer it from the soundness witness's type at a use site.
 promote :
-  ∀ {wℓ} {A : Set} {s : StoredClaim {wℓ = wℓ} A} →
+  ∀ {wℓ} {A : Set} (s : StoredClaim {wℓ = wℓ} A) →
   Soundness (StoredClaim.warr s) →
   ReceiptOn (StoredClaim.warr s)
-promote {s = storedClaim _ t} snd = receiptOn t snd
+promote (storedClaim _ t) snd = receiptOn t snd
 
 -- ── The legacy record ──────────────────────────────────────────────────
 --
diff --git a/verification/proofs/agda/Burrow/Trust.agda b/verification/proofs/agda/Burrow/Trust.agda
index 7db6ddd..130d697 100644
--- a/verification/proofs/agda/Burrow/Trust.agda
+++ b/verification/proofs/agda/Burrow/Trust.agda
@@ -39,7 +39,7 @@
 
 module Burrow.Trust where
 
-open import Agda.Primitive using (Level; lsuc; _⊔_)
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
 open import Data.Empty using (⊥)
 open import Data.Unit using (⊤; tt)
 
@@ -98,19 +98,11 @@ receipt-is-factive :
   ReceiptOn warr → A
 receipt-is-factive (receiptOn e (soundness v)) = v e
 
--- An unvalidated token is not factive, by construction: there is no
--- elimination for `Epi` that reaches `A`.
-epi-is-not-factive :
-  ∀ {wℓ} {A : Set} {warr : Warrant {wℓ = wℓ} A} →
-  ¬ (Epi {wℓ = wℓ} A → A) →
-  ¬ (Epi {wℓ = wℓ} A → A)
-epi-is-not-factive = λ f → f
-
 -- Re-validation lifts a token to the fact.  This is the positive form of
 -- the ledger read rule: a stored `extra.receipt` counts only once
 -- `Soundness` exists for it.
 revalidate :
-  ∀ {wℓ} {A : Set} {warr : Warrant {wℓ = wℓ} A} →
+  ∀ {wℓ} {A : Set} →
   (e : Epi {wℓ = wℓ} A) →
   Soundness (Epi.warrant e) →
   A
@@ -186,6 +178,14 @@ legacy-token = marker-printed
 legacy-epi : Epi (Checked marker)
 legacy-epi = epi legacy-warrant marker-printed
 
+-- An unvalidated token is not factive: no uniform function takes every
+-- token to the fact it purports to support, because the legacy token
+-- would then yield `Checked marker`, which is empty.  (This replaces a
+-- statement of the form `¬ X → ¬ X`, which was the identity function and
+-- said nothing; proof audit 2026-11-09.)
+epi-is-not-factive : ¬ (∀ {A : Set} → Epi {wℓ = lzero} A → A)
+epi-is-not-factive f = not-checked-at-marker (f legacy-epi)
+
 -- …and no soundness witness for it can exist.  This is the formal content
 -- of "a warrant, not a receipt".
 no-legacy-soundness : ¬ Soundness legacy-warrant
diff --git a/verification/proofs/agda/burrow.agda-lib b/verification/proofs/agda/burrow.agda-lib
new file mode 100644
index 0000000..6b1c382
--- /dev/null
+++ b/verification/proofs/agda/burrow.agda-lib
@@ -0,0 +1,3 @@
+name: burrow
+include: .
+depend: standard-library-2.1