From 7f673e7699c0bd0706a6af823a1725e3308975a6 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 14:30:25 +0000
Subject: [PATCH 1/6] ci(proofs): gate T-RECEIPT in CI and record the two
 deliberate hatches
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- proof-safety.yml: new `agda` job installs Agda 2.7.0.1 (archive digest
  checked; the same pin as the estate CI jobs) and runs
  scripts/check-agda-proofs.sh, which prints the receipt. New `rocq` job
  compiles the Rocq recheck candidate and requires every Print Assumptions
  line to report a closed term. actions.lock is unchanged: both jobs use
  the already-locked checkout.
- check-agda-proofs.sh: pin moves to 2.7.0.1, the release with a recorded
  digest; 2.8.0.2 stays the target until its digest is recorded.
- proof-debt.adoc: the two TBD hatches are the negative fixtures
  admitted_stub.v:11 and sorry_stub.lean:7, which protocol_contract
  asserts are detected.
- PROOF-STATUS.adoc: drop the stale "working-tree candidates, not
  committed" claim, say ungraded per PROOF-POLICY §8 rather than
  "Grade 3", and state that statuses move only on observed CI output.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
---
 .github/workflows/proof-safety.yml | 48 ++++++++++++++++++++++++++++++
 docs/PROOF-STATUS.adoc             | 37 ++++++++++++++---------
 docs/proof-debt.adoc               | 42 +++++++++++++++++---------
 scripts/check-agda-proofs.sh       |  7 +++--
 4 files changed, 104 insertions(+), 30 deletions(-)

diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml
index b145f55..4114366 100644
--- a/.github/workflows/proof-safety.yml
+++ b/.github/workflows/proof-safety.yml
@@ -26,3 +26,51 @@ 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 --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
+      - name: Compile T-RECEIPT-ROCQ and print its assumptions
+        working-directory: proofs/theory/rocq
+        run: |
+          set -euo pipefail
+          coqc --version
+          echo "commit: $GITHUB_SHA"
+          sha256sum ReceiptBoundary.v
+          out=$(coqc ReceiptBoundary.v)
+          printf '%s\n' "$out"
+          # Every Print Assumptions line must report a closed term.
+          test "$(printf '%s\n' "$out" | grep -c '^Closed under the global context$')" -eq 3
diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc
index fd85057..bcd9d3a 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,12 @@ 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.
+No transport or checked statement correspondence (PROOF-POLICY §2.2
+`RECONCILED`) exists, so neither leg counts toward a grade. 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 +92,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 +157,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 +168,8 @@ 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; a status moves only on their observed output.
 
 Completion requires: actual checker receipts; backend protocol agreement;
 production routing and provenance migration; implementation/interface proofs;
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)

From 9c6eb1bfd31627bf7cf0b595d714293ad6293b4a Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 14:53:52 +0000
Subject: [PATCH 2/6] ci(proofs): restrict the toolchain downloads to HTTPS,
 redirects included

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
---
 .github/workflows/proof-safety.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml
index 4114366..3cc276f 100644
--- a/.github/workflows/proof-safety.yml
+++ b/.github/workflows/proof-safety.yml
@@ -39,7 +39,7 @@ jobs:
           set -euo pipefail
           tc="$RUNNER_TEMP/agda"
           mkdir -p "$tc"
-          curl --fail --location --retry 3 -o "$tc/agda.tar.xz" \
+          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"

From 92bb6f72aa9b24525667fc62ae39956b31d64878 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 14:56:02 +0000
Subject: [PATCH 3/6] =?UTF-8?q?docs(proofs):=20record=20the=20=C2=A72.2=20?=
 =?UTF-8?q?statement=20comparison=20for=20T-RECEIPT?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

PROOF-POLICY §2.2 requires a recorded comparison of each recheck leg's
statement with the Agda statement before that leg can be RECONCILED.
T-RECEIPT-CORRESPONDENCE.adoc compares the Rocq and Lean re-proofs with
ReceiptBoundary.agda: universes (Set / predicative Set / Type, none in
Prop), the four statements term by term, and the residual differences
(unit eta, prelude, no identity types). Both legs stay BRIDGE-PENDING:
Rocq until the new rocq job's kernel result is recorded, Lean until a
pinned Lean run exists.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
---
 docs/PROOF-STATUS.adoc             |   7 +-
 docs/T-RECEIPT-CORRESPONDENCE.adoc | 136 +++++++++++++++++++++++++++++
 2 files changed, 141 insertions(+), 2 deletions(-)
 create mode 100644 docs/T-RECEIPT-CORRESPONDENCE.adoc

diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc
index bcd9d3a..7d12ab7 100644
--- a/docs/PROOF-STATUS.adoc
+++ b/docs/PROOF-STATUS.adoc
@@ -44,8 +44,11 @@ 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.
-No transport or checked statement correspondence (PROOF-POLICY §2.2
-`RECONCILED`) exists, so neither leg counts toward a grade. A Prop-only reformulation of Set-level quantification
+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
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).

From f30f6295e30b49f03bfbbfb9e693b7c974542ebd Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 16:19:01 +0000
Subject: [PATCH 4/6] ci(proofs): check each Rocq theorem's closure; record the
 Coq package

Review on #196 (CodeRabbit):
- The rocq job counted three "Closed under the global context" lines, so
  one theorem's output could stand in for another's. Each theorem now gets
  its own Print Assumptions query whose output must be exactly a closed
  term. Tested locally; a theorem resting on an axiom fails it.
- The job prints the installed coq package version and the archive's
  published SHA-256 for it. PROOF-STATUS records the deviation: a signed
  distribution package, not a pinned release archive.
- PROOF-STATUS: each status moves on its own required evidence, not only on
  the Agda and Rocq jobs' output.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
---
 .github/workflows/proof-safety.yml | 18 ++++++++++++++----
 docs/PROOF-STATUS.adoc             | 11 ++++++++++-
 2 files changed, 24 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml
index 3cc276f..d4ae278 100644
--- a/.github/workflows/proof-safety.yml
+++ b/.github/workflows/proof-safety.yml
@@ -63,6 +63,11 @@ jobs:
           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: |
@@ -70,7 +75,12 @@ jobs:
           coqc --version
           echo "commit: $GITHUB_SHA"
           sha256sum ReceiptBoundary.v
-          out=$(coqc ReceiptBoundary.v)
-          printf '%s\n' "$out"
-          # Every Print Assumptions line must report a closed term.
-          test "$(printf '%s\n' "$out" | grep -c '^Closed under the global context$')" -eq 3
+          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 7d12ab7..9b34cfe 100644
--- a/docs/PROOF-STATUS.adoc
+++ b/docs/PROOF-STATUS.adoc
@@ -172,7 +172,16 @@ 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. The `agda` and `rocq` jobs in `proof-safety.yml` are the
-theory gates; a status moves only on their observed output.
+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, but the version can move with the runner image. 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;

From 97b19a6f2e654cc8bf0af34a9bc35ef22604be81 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 16:19:16 +0000
Subject: [PATCH 5/6] ci(proofs): fail the rocq job unless the kernel is Coq
 8.18.x

Review on #196: assert the toolchain version, not only record it.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
---
 .github/workflows/proof-safety.yml | 4 +++-
 docs/PROOF-STATUS.adoc             | 3 ++-
 2 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml
index d4ae278..bb6acdd 100644
--- a/.github/workflows/proof-safety.yml
+++ b/.github/workflows/proof-safety.yml
@@ -72,7 +72,9 @@ jobs:
         working-directory: proofs/theory/rocq
         run: |
           set -euo pipefail
-          coqc --version
+          # Pinned at major.minor: a runner image that ships another Coq fails
+          # here instead of silently changing the kernel.
+          coqc --version | tee /dev/stderr | grep -q '^The Coq Proof Assistant, version 8\.18\.'
           echo "commit: $GITHUB_SHA"
           sha256sum ReceiptBoundary.v
           coqc -Q . TR ReceiptBoundary.v
diff --git a/docs/PROOF-STATUS.adoc b/docs/PROOF-STATUS.adoc
index 9b34cfe..f946702 100644
--- a/docs/PROOF-STATUS.adoc
+++ b/docs/PROOF-STATUS.adoc
@@ -180,7 +180,8 @@ 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, but the version can move with the runner image. A pinned Rocq
+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;

From 5d375a31eae46669b4ff6bc4aab245ef847502b5 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 9 Nov 2026 16:19:25 +0000
Subject: [PATCH 6/6] ci(proofs): check the Coq version without a pipe that
 pipefail could trip

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3
---
 .github/workflows/proof-safety.yml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.github/workflows/proof-safety.yml b/.github/workflows/proof-safety.yml
index bb6acdd..94944c0 100644
--- a/.github/workflows/proof-safety.yml
+++ b/.github/workflows/proof-safety.yml
@@ -74,7 +74,9 @@ jobs:
           set -euo pipefail
           # Pinned at major.minor: a runner image that ships another Coq fails
           # here instead of silently changing the kernel.
-          coqc --version | tee /dev/stderr | grep -q '^The Coq Proof Assistant, version 8\.18\.'
+          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