diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml
index b145f55..94944c0 100644
--- a/.github/workflows/proof-safety.yml
+++ b/.github/workflows/proof-safety.yml
@@ -26,3 +26,65 @@ jobs:
           cargo test --locked --test protocol_contract
           cargo test --locked --bin echidnabot clone_contract_tests
           cargo test --locked --lib git_process_tests
+  agda:
+    name: Agda theory (PROOF-POLICY §2.1 canonical invocation)
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
+      - name: Install pinned, digest-checked Agda
+        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
+          tar --no-same-owner -xJf "$tc/agda.tar.xz" -C "$tc"
+          {
+            echo "Agda_datadir=$tc/Agda-v2.7.0.1/data"
+            echo "LC_ALL=C.UTF-8"
+          } >> "$GITHUB_ENV"
+          echo "$tc/Agda-v2.7.0.1/bin" >> "$GITHUB_PATH"
+      - name: Type-check T-RECEIPT and the fixture identity, printing the receipt
+        run: ./scripts/check-agda-proofs.sh
+  rocq:
+    name: Rocq recheck candidate (kernel acceptance only)
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@v7.0.1
+        with:
+          persist-credentials: false
+      - name: Install the distribution Rocq (Coq) kernel
+        run: |
+          set -euo pipefail
+          sudo apt-get update -q
+          sudo apt-get install -y -q --no-install-recommends coq
+          # Toolchain record: a signed Ubuntu archive package, not a pinned
+          # release archive (see docs/PROOF-STATUS.adoc). Print the installed
+          # version and the archive's published SHA-256 for that version.
+          echo "coq package: $(dpkg-query -W -f='${Version}' coq)"
+          apt-cache show "coq=$(dpkg-query -W -f='${Version}' coq)" | grep -m1 '^SHA256:'
+      - name: Compile T-RECEIPT-ROCQ and print its assumptions
+        working-directory: proofs/theory/rocq
+        run: |
+          set -euo pipefail
+          # Pinned at major.minor: a runner image that ships another Coq fails
+          # here instead of silently changing the kernel.
+          v=$(coqc --version)
+          printf '%s\n' "$v"
+          grep -q '^The Coq Proof Assistant, version 8\.18\.' <<<"$v"
+          echo "commit: $GITHUB_SHA"
+          sha256sum ReceiptBoundary.v
+          coqc -Q . TR ReceiptBoundary.v
+          # Check each theorem on its own: its Print Assumptions output must be
+          # exactly a closed term, so one theorem cannot pass for another.
+          for t in receive_with_soundness no_unconditional_reflection no_soundness_for_empty_token; do
+            printf 'From TR Require Import ReceiptBoundary.\nPrint Assumptions %s.\n' "$t" > "Check_$t.v"
+            out=$(coqc -Q . TR "Check_$t.v")
+            echo "$t: $out"
+            test "$out" = "Closed under the global context"
+          done
diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc
index fd85057..f946702 100644
--- a/docs/PROOF-STATUS.adoc
+++ b/docs/PROOF-STATUS.adoc
@@ -4,12 +4,12 @@
 
 == Evidence rules
 
-Updated 2026-11-01 on `arena/68c18146-echidnabot`, based on
-`ab26bd54c8bdc04da8cc48c0778a25eb774be268`. New files are working-tree
-candidates, not committed or checked proof receipts. No Grade 3 attainment
-is claimed. `open` means not checked/done, `argued` means an explicit
-assumption, and `tested-only` requires an actual observed bounded check.
-ConfidenceLevel::Level3 is a runtime heuristic, NOT Mathesis Grade 3.
+The theory sources below were committed in #191 (`eedfdc3`). No proof
+witness grade is claimed: under PROOF-POLICY §8 a grade is derived from a
+CI receipt, and T-RECEIPT has none yet, so it is `ungraded`. `open` means
+not checked/done, `argued` means an explicit assumption, and `tested-only`
+requires an actual observed bounded check. ConfidenceLevel::Level3 is a
+runtime heuristic, NOT a proof witness grade (`PWG-3`).
 
 Policies and pinned references are in
 link:ESTATE-ROUTING-AUDIT.adoc[the routing audit]. Theory requires strict
@@ -26,7 +26,10 @@ a mathematical model does not establish runtime refinement.
 |A general evidence token does not imply its claim;
 `proofs/agda/ReceiptBoundary.agda`
 |open
-|AGDA-PENDING. `no-unconditional-reflection` constructs a contradiction
+|Awaiting the CI receipt from the `agda` job in
+`.github/workflows/proof-safety.yml` (pinned, digest-checked Agda 2.7.0.1,
+`scripts/check-agda-proofs.sh`). Unpinned local observation only: Agda 2.6.3
+accepts the module under the same flags. `no-unconditional-reflection` constructs a contradiction
 from unconditional reflection by instantiating Claim with Empty and evidence
 with Unit. `receive-with-soundness` requires an explicit evidence-to-claim
 function. This is new local theory, informed by epistemic-types, NOT a port
@@ -37,8 +40,15 @@ T-RECEIPT
 |open
 |Independent re-proof source candidates now exist under
 `proofs/theory/{rocq,lean}/ReceiptBoundary.*`, without libraries, axioms or
-admitted obligations. Neither was compiled; no transport or checked
-correspondence exists. A Prop-only reformulation of Set-level quantification
+admitted obligations. The `rocq` job in `proof-safety.yml` compiles the
+Rocq candidate and requires `Print Assumptions` to report closed terms;
+that is kernel acceptance, not correspondence (unpinned local observation:
+Coq 8.18.0 accepts it). The Lean candidate has no CI job and is unchecked.
+Both are re-proofs, not transports. The statement comparison PROOF-POLICY
+§2.2 asks for is recorded in
+link:T-RECEIPT-CORRESPONDENCE.adoc[`T-RECEIPT-CORRESPONDENCE.adoc`]. Both legs
+stay `BRIDGE-PENDING`, and count toward no grade, until a kernel result is
+recorded against it. A Prop-only reformulation of Set-level quantification
 is not silently interchangeable. The candidates deliberately use Rocq Set
 and Lean Type rather than silently shrinking the claims to Prop.
 |E-ADAPTER
@@ -85,10 +95,10 @@ is out of scope does NOT make that scaffolding verified.
   because there was no Agda record. It is not witness transport. Rocq/Lean
   Prop and Agda Set differ; correspondence is limited to propositional
   identity and remains `open` until checked and justified explicitly.
-  All three current executions are unavailable in this sandbox.
 * `proofs/coq/admitted_stub.v` and `proofs/lean/sorry_stub.lean` are negative
   fixtures, not candidate proofs. Their escape hatches must stay intact.
-  They are excluded from Grade 3 counts, not repaired into passing fixtures.
+  They are excluded from every proof count and grade, not repaired into
+  passing fixtures. `docs/proof-debt.adoc` records both.
 * JSON files under `proofs/test_fixtures` are webhook/prover inputs, not proofs.
 
 === ABI scaffold debt (not verified)
@@ -150,7 +160,9 @@ this is an unmet latest-stable target, not a completed upgrade.
 
 == Reproduction and completion criteria
 
-`./scripts/check-agda-proofs.sh` requires exactly Agda 2.8.0.2, ignores stale
+`./scripts/check-agda-proofs.sh` requires exactly Agda 2.7.0.1 (the CI pin,
+whose archive digest is recorded in `proof-safety.yml`; 2.8.0.2 remains the
+latest-stable target until its digest is recorded), ignores stale
 interfaces, uses no external libraries, and runs the strict policy flags.
 It prints source hashes, base revision and invocations. Capture the output
 and record the observed result here; do not edit statuses based on expected
@@ -159,8 +171,18 @@ This is evidence that absence is not silently skipped, not a proof execution.
 
 `cargo test --locked dispatcher::verisim_echidna` and the existing protocol
 suites remain unrun. Creusot, Idris2 and independent theory rechecks also
-remain unrun. CI wiring for the new theory gate and its real positive/negative
-controls is still open; a local check command is not an installed CI gate.
+remain unrun. The `agda` and `rocq` jobs in `proof-safety.yml` are the
+theory gates. Each status moves only when its own required evidence is
+observed: the theory rows on those jobs' output, the Rust rows on a Creusot
+check, and so on.
+
+Toolchain deviation (Rocq): the `rocq` job installs Coq from the signed
+Ubuntu 24.04 archive, not from a pinned release archive with a recorded
+digest. The job prints the installed package version and the archive's
+published SHA-256 for it, so each run records exactly which kernel accepted
+the file. It fails unless the kernel is Coq 8.18.x, so a runner-image change
+cannot silently swap kernels. A pinned Rocq
+release replaces this when one is available to CI.
 
 Completion requires: actual checker receipts; backend protocol agreement;
 production routing and provenance migration; implementation/interface proofs;
diff --git a/docs/T-RECEIPT-CORRESPONDENCE.adoc b/docs/T-RECEIPT-CORRESPONDENCE.adoc
new file mode 100644
index 0000000..2a14d02
--- /dev/null
+++ b/docs/T-RECEIPT-CORRESPONDENCE.adoc
@@ -0,0 +1,136 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= T-RECEIPT: statement correspondence (PROOF-POLICY §2.2)
+:toc:
+
+This record compares the Agda statement of T-RECEIPT with its Rocq and Lean
+re-proofs, as PROOF-POLICY §2.2 requires before a recheck leg can count
+toward a grade. It records the comparison only. A leg is `RECONCILED` when
+this comparison exists *and* its kernel has accepted it, so each leg's state
+below depends on an observed run, not on this text.
+
+== Sources
+
+[cols="1,3,2",options="header"]
+|===
+|Prover |File |Mode
+
+|Agda (source of truth)
+|`proofs/agda/ReceiptBoundary.agda`
+|`--safe --without-K --cubical-compatible --exact-split --no-sized-types
+--no-guardedness`, no libraries
+
+|Rocq
+|`proofs/theory/rocq/ReceiptBoundary.v`
+|`re-proved`, no libraries beyond the prelude loaded by default
+
+|Lean
+|`proofs/theory/lean/ReceiptBoundary.lean`
+|`re-proved`, core only, no Mathlib
+|===
+
+Both legs are independent re-proofs. Neither is transported, so neither
+depends on a translator.
+
+== Universe and type discipline
+
+[cols="2,2,2,2",options="header"]
+|===
+|Notion |Agda |Rocq |Lean
+
+|Claims and evidence
+|`Set` (`Set₀`)
+|`Set`, predicative (no `-impredicative-set`)
+|`Type` (`Sort 1`)
+
+|The warrant record
+|`Warrant : Set → Set₁`
+|`ReceiptWarrant : Set → Type`, a universe above `Set`
+|`ReceiptWarrant : Type → Type 1`
+
+|The soundness record
+|`SoundWarrant w : Set`
+|`SoundReceiptWarrant w : Type`
+|`SoundReceiptWarrant w : Type`
+
+|Empty claim
+|`data Empty : Set` (no constructors)
+|`Empty_set : Set` (prelude, no constructors)
+|`Empty : Type` (core, no constructors)
+
+|Unit evidence
+|`record Unit : Set` (eta holds)
+|`unit : Set` (inductive, no definitional eta)
+|`Unit` = `PUnit.{1}` (structure eta holds)
+|===
+
+None of the three uses `Prop`. That is deliberate: a `Prop`-only
+reformulation would quantify over a different class of claims, and §2.2 asks
+for the same proposition, not a weaker one.
+
+== Propositions compared
+
+Implicit arguments are shown in braces in every column.
+
+[cols="1,3",options="header"]
+|===
+|Theorem |Statement in all three provers
+
+|`receive-with-soundness` / `receive_with_soundness` / `receiveWithSoundness`
+|For every claim `{Claim}` in the base universe, every warrant `w` for it and
+every soundness witness for `w`, there is an inhabitant of `Claim`.
+
+|`empty-claim-token` / `empty_claim_token` / `emptyClaimToken`
+|A warrant for the empty claim whose evidence type is the unit type and whose
+evidence is its constructor. This is a definition, compared so that the next
+two theorems refer to the same object.
+
+|`no-unconditional-reflection` / `no_unconditional_reflection` /
+`noUnconditionalReflection`
+|A function that, for every claim in the base universe, turns any warrant for
+it into an inhabitant of the claim, yields an inhabitant of the empty type.
+
+|`no-soundness-for-empty-token` / `no_soundness_for_empty_token` /
+`noSoundnessForEmptyToken`
+|A soundness witness for `empty-claim-token` yields an inhabitant of the empty
+type.
+|===
+
+The quantifier structure, the argument order and the result type match
+term for term. The proofs are also the same terms: application of the
+soundness field to the evidence field, and instantiation of the reflection
+function at the empty claim.
+
+== Residual assumptions and differences
+
+* *Unit eta.* Rocq's `unit` has no definitional eta, while Agda's `Unit` and
+  Lean's `Unit` do. No statement or proof here inspects or compares unit
+  values, so the difference is not used.
+* *Prelude.* Rocq loads `Init` by default, and Lean loads its core. Both
+  supply only inductive definitions here (`Empty_set`, `unit`, `Empty`,
+  `PUnit`). The files print their assumption sets: Rocq with
+  `Print Assumptions`, Lean with `#print axioms`.
+* *Equality and K.* No statement uses identity types, so `--without-K` in
+  Agda has no counterpart obligation in either target.
+* *No claim about Rust.* As in the Agda source, nothing here describes the
+  Rust receipt parser or any network behaviour.
+
+== Correspondence state
+
+[cols="1,2,3",options="header"]
+|===
+|Leg |State |What moves it
+
+|Rocq
+|`BRIDGE-PENDING`
+|The comparison above is recorded. It becomes `RECONCILED` when the `rocq`
+job in `.github/workflows/proof-safety.yml` records a kernel acceptance with
+all three `Print Assumptions` closed, on the commit that carries this record.
+
+|Lean
+|`BRIDGE-PENDING`
+|The comparison above is recorded. No pinned Lean run exists yet, so there is
+no kernel result to reconcile against.
+|===
+
+A leg still `BRIDGE-PENDING` does not count toward a Proof Witness Grade
+(PROOF-POLICY §8.2).
diff --git a/docs/proof-debt.adoc b/docs/proof-debt.adoc
index a61d06b..688d15b 100644
--- a/docs/proof-debt.adoc
+++ b/docs/proof-debt.adoc
@@ -1,22 +1,36 @@
 == Proof Debt
 
 Tracks soundness-relevant escape hatches in `+echidnabot+` that the
-trusted-base reducer flags as undocumented. Each is retained pending
-dedicated cleanup; new occurrences should land with an inline
-`+// TRUSTED:+` annotation or an entry below.
+trusted-base reducer flags. New occurrences land with an inline
+`+// TRUSTED:+` annotation or an entry below, following the estate
+`TRUSTED-BASE-REDUCTION-POLICY.adoc`.
 
-=== Current entries (placeholder)
+=== Current entries
 
-The current 2 escape hatches were inherited from earlier scaffolding and
-have not yet been individually classified. Tracking issue: filed
-alongside this PR.
+Both hatches are deliberate negative fixtures. They are not debt to be
+repaid: removing either escape hatch would break the test that proves the
+detector sees it. They are excluded from every proof count and grade.
 
-* Hatch 1: TBD (file:line)
-* Hatch 2: TBD (file:line)
+[cols="2,1,4",options="header"]
+|===
+|Location |Hatch |Rationale
 
-=== How to populate
+|`proofs/coq/admitted_stub.v:11`
+|`Admitted.`
+|Negative fixture. `tests/protocol_contract.rs`
+(`checked_in_negative_proofs_are_detected`) asserts that echidnabot's axiom
+scanner reports it. Keep the hatch intact.
 
-Run the standards trusted-base reducer locally; it lists the offending
-file:line tuples. Move each from "`TBD`" to a real entry with a one-line
-rationale. When all entries have rationale + cleanup-issue link, this
-file is fully load-bearing instead of a placeholder.
+|`proofs/lean/sorry_stub.lean:7`
+|`sorry`
+|Negative fixture, same test. Carries an inline
+`hypatia: allow code_safety/sorry` directive with this rationale.
+|===
+
+=== Not hatches, but not proofs either
+
+`src/abi/{Types,Layout,Foreign}.idr` is unfilled template scaffolding
+(`{{PROJECT}}` module names and open holes). It contains no
+`believe_me`, `assert_total` or `postulate`, so the reducer does not list
+it, but it is not a verified ABI. See `docs/PROOF-STATUS.adoc`,
+"ABI scaffold debt".
diff --git a/scripts/check-agda-proofs.sh b/scripts/check-agda-proofs.sh
index 4ea20c0..b052b13 100755
--- a/scripts/check-agda-proofs.sh
+++ b/scripts/check-agda-proofs.sh
@@ -4,9 +4,12 @@
 set -euo pipefail
 cd "$(dirname "${BASH_SOURCE[0]}")/.."
 
-expected='Agda version 2.8.0.2'
+# Pinned to the release whose archive digest is recorded in
+# .github/workflows/proof-safety.yml (the estate CI pin). 2.8.0.2 stays the
+# latest-stable target until its digest is recorded beside that job.
+expected='Agda version 2.7.0.1'
 if ! command -v agda >/dev/null; then
-    echo 'OPEN: Agda 2.8.0.2 is required; no proof was checked.' >&2
+    echo 'OPEN: Agda 2.7.0.1 is required; no proof was checked.' >&2
     exit 127
 fi
 actual=$(agda --version)