diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml
index c276766..7e3b141 100644
--- a/.github/workflows/proof-safety.yml
+++ b/.github/workflows/proof-safety.yml
@@ -64,3 +64,55 @@ jobs:
           ECHIDNA_BIN: ${{ github.workspace }}/_echidna/target/debug/echidna
         run: |
           bash tests/e2e.sh
+  agda:
+    name: Agda proofs (PROOF-POLICY §2.1 canonical invocation)
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - name: Install pinned, digest-checked Agda and standard library
+        run: |
+          set -euo pipefail
+          tc="$RUNNER_TEMP/agda"
+          mkdir -p "$tc"
+          curl --proto '=https' --proto-redir '=https' --fail --location --retry 3 -o "$tc/agda.tar.xz" \
+            https://github.com/agda/agda/releases/download/v2.7.0.1/Agda-v2.7.0.1-linux.tar.xz
+          echo "975b515a14877ab6bce5bfc641e16c4a3ee52ca5d7f846577dee80aa2145db8a  $tc/agda.tar.xz" | sha256sum --check
+          curl --proto '=https' --proto-redir '=https' --fail --location --retry 3 -o "$tc/stdlib.tar.gz" \
+            https://github.com/agda/agda-stdlib/archive/refs/tags/v2.1.tar.gz
+          echo "72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431  $tc/stdlib.tar.gz" | sha256sum --check
+          tar --no-same-owner -xJf "$tc/agda.tar.xz" -C "$tc"
+          tar --no-same-owner -xzf "$tc/stdlib.tar.gz" -C "$tc"
+          printf '%s\n' "$tc/agda-stdlib-2.1/standard-library.agda-lib" \
+            "$GITHUB_WORKSPACE/verification/proofs/agda/burrow.agda-lib" > "$tc/libraries"
+          {
+            echo "Agda_datadir=$tc/Agda-v2.7.0.1/data"
+            echo "AGDA_LIBRARIES_FILE=$tc/libraries"
+            echo "LC_ALL=C.UTF-8"
+          } >> "$GITHUB_ENV"
+          echo "$tc/Agda-v2.7.0.1/bin" >> "$GITHUB_PATH"
+      - name: Type-check DOM-1 and DOM-2 and print the receipt
+        working-directory: verification/proofs/agda
+        run: |
+          set -euo pipefail
+          agda --version
+          echo "commit: $GITHUB_SHA"
+          echo "flags: --safe --without-K --cubical-compatible"
+          echo "stdlib: agda-stdlib v2.1, archive sha256 72ca3ea25094efa0439e106f0d949330414232ec4cc5c3c3316e7e70dd06d431"
+          echo "first-party sources:"
+          sha256sum Burrow/Trust.agda Burrow/Ledger.agda burrow.agda-lib
+          stdlib="$RUNNER_TEMP/agda/agda-stdlib-2.1"
+          find . "$stdlib" -name '*.agdai' -delete
+          for m in Burrow/Trust.agda Burrow/Ledger.agda; do
+            agda --no-default-libraries --library-file "$AGDA_LIBRARIES_FILE" \
+              --safe --without-K --cubical-compatible "$m"
+          done
+          # The transitive import cone is exactly the set of interfaces this
+          # check wrote. --safe is coinfective, so every module in it was
+          # itself checked under --safe: no postulate, no unsafe pragma.
+          echo "import cone (standard-library modules, sources pinned by the archive digest):"
+          find "$stdlib" -name '*.agdai' | sed "s|.*/agda/||; s|^src/||; s|\.agdai$||; s|/|.|g" | LC_ALL=C sort
+          echo "import cone (first-party modules):"
+          find . -name '*.agdai' | sed "s|.*/agda/||; s|^src/||; s|\.agdai$||; s|/|.|g" | LC_ALL=C sort
diff --git a/.gitignore b/.gitignore
index 4ce862d..2161e8e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -118,3 +118,10 @@ dist/
 /exports/*.lgt
 composer/*.beam
 composer/build/
+
+# Coq/Rocq build artefacts (written by `just proof-check-coq`)
+*.vo
+*.vok
+*.vos
+*.glob
+.*.aux
diff --git a/CLAUDE.md b/CLAUDE.md
index dab6e6d..68ceab6 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 (PROOF-POLICY §1.2) |
 | APIs, ABIs, wire formats, engineering properties | Idris2 |
 | Theory (anything true of any implementation) | Agda, rechecked in Rocq and Lean |
 
@@ -53,10 +53,15 @@ 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 Witness Grades (PROOF-POLICY §8, normative; always write the `PWG-`
+  prefix): `PWG-3` = the Agda source is checked under the §2.1 invocation
+  with a receipt (Agda version, stdlib pin, flags, import cone);
+  `PWG-2i` = plus one counted Rocq or Lean recheck (kernel-accepted and
+  §2.2 `RECONCILED`); `PWG-2ii` = plus both; `PWG-1` = every counted
+  witness has a current per-commit receipt from a headless, pinned run.
+  Engineering proofs (Creusot, Verus, SPARK, Idris2) carry no PWG (§8.1).
+  Grades are derived from receipts, never asserted, and never flattened
+  into 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 +69,10 @@ 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: 2 of 14 tracked obligations proven (DOM-1, DOM-2,
+first-party Agda). Both are `ungraded` until the `agda` job in
+`.github/workflows/proof-safety.yml` has produced a receipt for the current
+`main` commit; `PWG-3` follows from that receipt, not from this sentence, and
+lapses if a later run on `main` fails or cannot be reproduced. 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..e9bf0a0 100644
--- a/Justfile
+++ b/Justfile
@@ -1342,8 +1342,19 @@ help-me:
 # ═══════════════════════════════════════════════════════════════════════════════
 
 # Check all formal proofs (Idris2 + Lean4 + Agda + Coq)
-proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous
-    @echo "=== All proof checks complete ==="
+# Runs every checker even when an earlier one fails, then fails if any did.
+proof-check-all:
+    #!/usr/bin/env bash
+    set -uo pipefail
+    failed=()
+    for r in proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous; do
+        just "$r" || failed+=("$r")
+    done
+    if [ ${#failed[@]} -gt 0 ]; then
+        echo "=== Proof checks FAILED or NOT RUN: ${failed[*]} ===" >&2
+        exit 1
+    fi
+    echo "=== All proof checks complete ==="
 
 # Check Idris2 proofs (ABI, types, dependent type proofs)
 proof-check-idris2:
@@ -1351,8 +1362,8 @@ proof-check-idris2:
     set -euo pipefail
     echo "=== Checking Idris2 proofs ==="
     if ! command -v idris2 &>/dev/null; then
-        echo "SKIP: idris2 not installed"
-        exit 0
+        echo "NOT RUN: idris2 not installed — a missing prover is an open obligation, not a pass (PROOF-POLICY §2.1)" >&2
+        exit 1
     fi
     ERRORS=0
     for f in $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null); do
@@ -1376,8 +1387,8 @@ proof-check-lean4:
     set -euo pipefail
     echo "=== Checking Lean4 proofs ==="
     if ! command -v lean &>/dev/null; then
-        echo "SKIP: lean not installed"
-        exit 0
+        echo "NOT RUN: lean not installed — a missing prover is an open obligation, not a pass (PROOF-POLICY §2.1)" >&2
+        exit 1
     fi
     ERRORS=0
     for f in $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null); do
@@ -1401,8 +1412,8 @@ proof-check-agda:
     set -euo pipefail
     echo "=== Checking Agda proofs ==="
     if ! command -v agda &>/dev/null; then
-        echo "SKIP: agda not installed"
-        exit 0
+        echo "NOT RUN: agda not installed — a missing prover is an open obligation, not a pass (PROOF-POLICY §2.1)" >&2
+        exit 1
     fi
     # Estate canonical invocation (standards 3-practice/PROOF-POLICY.adoc
     # §2.1). `--cubical-compatible` implies `--without-K`; both are named
@@ -1441,8 +1452,8 @@ proof-check-coq:
     set -euo pipefail
     echo "=== Checking Coq proofs ==="
     if ! command -v coqc &>/dev/null; then
-        echo "SKIP: coqc not installed"
-        exit 0
+        echo "NOT RUN: coqc not installed — a missing prover is an open obligation, not a pass (PROOF-POLICY §2.1)" >&2
+        exit 1
     fi
     ERRORS=0
     for f in $(find verification/proofs/coq -name '*.v' 2>/dev/null); do
diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc
index 1420dc8..68b3a50 100644
--- a/docs/proof-debt.adoc
+++ b/docs/proof-debt.adoc
@@ -22,9 +22,11 @@ reading of the situation.
 == (a) Discharged in this repo
 
 - `verification/proofs/agda/Burrow/Trust.agda` — the receipt/warrant
-  semantics (DOM-1). Grade 3: type-checks under
+  semantics (DOM-1). Mathesis Grade 3 on a historical local run: type-checks under
   `agda --safe --without-K --cubical-compatible`, 0 warnings, also clean
-  under full `--cubical`. Agda 2.7.0.1, agda-stdlib 2.4, 2026-11-01.
+  under full `--cubical`. Agda 2.7.0.1, agda-stdlib 2.4, 2026-11-01. Under
+  PROOF-POLICY §8 it is `ungraded` until the CI `agda` job (stdlib 2.1)
+  records a receipt for the current commit.
 - `verification/proofs/agda/Burrow/Ledger.agda` — the ledger read path and
   `no-launder` (DOM-2). Same toolchain, same flags, same date.
 
@@ -44,7 +46,9 @@ would be exactly the unfalsifiable "covered by tests" the policy rejects.
 
 - (none)
 
-No first-party proof exists, so no first-party axiom exists.
+The first-party proofs (DOM-1 `Burrow/Trust.agda`, DOM-2
+`Burrow/Ledger.agda`) check under `--safe`, which rejects `postulate`, so
+no first-party axiom exists.
 
 == 1. Debt
 
@@ -142,12 +146,19 @@ already retired for `TODO` markers — "grepping prose … measures the prose,
 not the proofs" — and it should be reported upstream rather than triaged
 here.
 
-The absence of markers is not a clean bill of health. It reflects an empty
-proof set: there is nothing to have escaped from.
+The absence of markers is not a clean bill of health. The only proofs are
+DOM-1 and DOM-2 in §(a). Their CI check runs under `--safe`, which rejects
+`postulate` and the unsafe pragmas and options (`TERMINATING`,
+`NON_TERMINATING`, `--type-in-type` and the like) in the whole import cone.
+That check and the marker scan are different things: the scan is textual and
+covers other languages' markers (`sorry`, `Admitted`, `believe_me`), which
+`--safe` neither knows nor replaces. Neither says anything about the twelve
+obligations that have no proof at all.
 
 == 3. What a Grade 3 result would look like here
 
-Mathesis §5: "A proof is Grade 3 if it type-checks locally in Agda but has
+This section uses the Mathesis grade, not the Proof Witness Grade of
+PROOF-POLICY §8 (`PWG-3`), which needs a CI receipt as well. Mathesis §5: "A proof is Grade 3 if it type-checks locally in Agda but has
 not been translated to an independent foundational system." For this
 repository the shortest honest path is one theorem about Burrower's own
 contract handling, checked with:
diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc
index 0e51571..c134211 100644
--- a/docs/status/PROOF-STATUS.adoc
+++ b/docs/status/PROOF-STATUS.adoc
@@ -17,10 +17,18 @@
 
 *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.
+Proof Witness Grade (`PROOF-POLICY` §8, normative): the two Domain proofs
+are `ungraded` until a receipt exists. A grade is derived from a receipt
+that records the Agda version, the standard-library pin, the flags in
+force and the import cone; the 2026-11-01 local run recorded the first
+three but no source commit or digests. The `agda` job in
+`.github/workflows/proof-safety.yml` (Agda 2.7.0.1 and agda-stdlib 2.1,
+both digest-pinned; canonical §2.1 flags; prints the commit and the
+SHA-256 of each first-party source) produces that receipt. The first green
+run on `main` makes them `PWG-3`, for as long as the receipt is current:
+a later failing or unreproducible run on `main` withdraws the grade. No Rocq or Lean recheck exists, so
+nothing can be higher. Nothing else in this repository is a theory
+theorem, so nothing else carries a PWG.
 
 === Proofs Done
 
@@ -34,8 +42,9 @@ repository has a grade.
  |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`
+|Historical local run only (no commit or digests recorded):
+ `agda --safe --without-K --cubical-compatible`, 0 warnings; also clean
+ under full `--cubical`. Current verification is the CI receipt.
 
 |DOM-2
 |Ledger read path: no function from a stored record to the fact exists
@@ -122,7 +131,7 @@ 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 (receipt pending; see above); DOM-3..7 added;
  `just proof-check-agda` moved to the estate canonical flags with an
  include path |Audit 2026-11-01
 |===
diff --git a/verification/proofs/agda/burrow.agda-lib b/verification/proofs/agda/burrow.agda-lib
new file mode 100644
index 0000000..f425fc0
--- /dev/null
+++ b/verification/proofs/agda/burrow.agda-lib
@@ -0,0 +1,5 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Agda library for proof-burrower's first-party proofs (DOM-1, DOM-2).
+name: burrow
+depend: standard-library
+include: .