diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock
index c612c82..ce7fcc1 100644
--- a/.github/workflows/actions.lock
+++ b/.github/workflows/actions.lock
@@ -3,6 +3,8 @@
 # Docs: https://gh.io/actions-lockfile
 version: 'v0.0.3'
 workflows:
+    '.github/workflows/agda-cross-project.yml':
+        - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
     '.github/workflows/boj-build.yml':
         - 'actions/checkout@v7.0.1'
     '.github/workflows/codeql.yml':
@@ -63,6 +65,11 @@ workflows:
     '.github/workflows/workflow-linter.yml':
         - 'actions/checkout@v7.0.1'
 dependencies:
+    'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1':
+        ref: 'v7.0.1'
+        commit: 'sha1-3d3c42e5aac5ba805825da76410c181273ba90b1'
+        owner_id: 44036562
+        repo_id: 197814629
     'actions/checkout@v7.0.1':
         ref: 'v7.0.1'
         commit: 'sha1-3d3c42e5aac5ba805825da76410c181273ba90b1'
diff --git a/.github/workflows/agda-cross-project.yml b/.github/workflows/agda-cross-project.yml
new file mode 100644
index 0000000..530c1a7
--- /dev/null
+++ b/.github/workflows/agda-cross-project.yml
@@ -0,0 +1,84 @@
+# SPDX-License-Identifier: MPL-2.0
+# Cross-project Agda compatibility gate. Pin external source revisions.
+name: Cross-project Agda Verification
+
+on:
+  pull_request:
+    paths:
+      - 'verification/proofs/agda/**'
+      - 'scripts/check-agda-verification.sh'
+      - '.github/workflows/agda-cross-project.yml'
+  push:
+    branches: [main]
+    paths:
+      - 'verification/proofs/agda/**'
+      - 'scripts/check-agda-verification.sh'
+      - '.github/workflows/agda-cross-project.yml'
+  workflow_dispatch:
+
+permissions:
+  contents: read
+
+concurrency:
+  group: agda-cross-project-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  typecheck:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 45
+    steps:
+      - name: Checkout
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+
+      # Use Ubuntu's GHC/Cabal packages rather than an additional
+      # marketplace setup action; the proof compiler itself is pinned.
+      - name: Install Haskell build toolchain
+        run: |
+          set -euo pipefail
+          sudo apt-get update -qq
+          sudo apt-get install -y --no-install-recommends ghc cabal-install
+          # Hosted runners also contain newer GHC versions whose 'base'
+          # package is incompatible with Agda 2.7.0.1. Choose the distro
+          # compiler explicitly, not the first ghc found on PATH.
+          /usr/bin/ghc --version
+          cabal --version
+
+      - name: Install Agda 2.7.0.1 and compatible stdlib 2.1.1
+        run: |
+          set -euo pipefail
+          cabal update
+          cabal install Agda-2.7.0.1 --with-compiler=/usr/bin/ghc --overwrite-policy=always
+          echo "$HOME/.cabal/bin" >> "$GITHUB_PATH"
+          curl -fsSL --retry 3 -o "$RUNNER_TEMP/agda-stdlib.tar.gz" \
+            https://github.com/agda/agda-stdlib/archive/refs/tags/v2.1.1.tar.gz
+          tar xzf "$RUNNER_TEMP/agda-stdlib.tar.gz" -C "$RUNNER_TEMP"
+          test -f "$RUNNER_TEMP/agda-stdlib-2.1.1/standard-library.agda-lib"
+
+      - name: Fetch pinned first-party Agda libraries
+        run: |
+          set -euo pipefail
+          mkdir -p "$RUNNER_TEMP/type-libs"
+          git clone --no-checkout https://github.com/hyperpolymath/absolute-zero.git "$RUNNER_TEMP/type-libs/absolute-zero"
+          git -C "$RUNNER_TEMP/type-libs/absolute-zero" checkout bb46232ea4dbc4b6ad2b97d2da6baebb3e026662
+          git clone --no-checkout https://github.com/hyperpolymath/echo-types.git "$RUNNER_TEMP/type-libs/echo-types"
+          git -C "$RUNNER_TEMP/type-libs/echo-types" checkout b0982c44f36133acd2d0e1d4e03cf031fff7a470
+
+      - name: Register exact proof library revisions
+        run: |
+          set -euo pipefail
+          agda --version
+          stdlib="$RUNNER_TEMP/agda-stdlib-2.1.1/standard-library.agda-lib"
+          test -f "$stdlib"
+          mkdir -p "$HOME/.agda"
+          printf '%s\n' \
+            "$stdlib" \
+            "$RUNNER_TEMP/type-libs/absolute-zero/absolute-zero.agda-lib" \
+            "$RUNNER_TEMP/type-libs/echo-types/echo-types.agda-lib" \
+            > "$HOME/.agda/libraries"
+          printf 'standard-library\n' > "$HOME/.agda/defaults"
+
+      - name: Check full Agda profile
+        run: bash scripts/check-agda-verification.sh
diff --git a/.github/workflows/workflow-linter.yml b/.github/workflows/workflow-linter.yml
index 2c216f1..c57d9b1 100644
--- a/.github/workflows/workflow-linter.yml
+++ b/.github/workflows/workflow-linter.yml
@@ -70,9 +70,10 @@ jobs:
           XDG_DATA_HOME: ${{ runner.temp }}/workflow-linter-data
         run: |
           # Binary extensions accept release tags, not source commit pins.
-          # Verify the v0.1.6 linux-amd64 release bytes before executing them.
-          gh release download v0.1.6 --repo github/gh-actions-lock --pattern linux-amd64 --output "$RUNNER_TEMP/gh-actions-lock"
-          echo "4181ec1da5408b34b9a542a7ee5c6ce3a4d6ac815c7d0206a00ceca8a817f4e3  $RUNNER_TEMP/gh-actions-lock" | sha256sum --check --strict
+          # v0.1.6 only parses lockfile v0.0.2, whereas this repo uses
+          # v0.0.3. Pin a compatible release AND the published asset digest.
+          gh release download v0.4.0 --repo github/gh-actions-lock --pattern linux-amd64 --output "$RUNNER_TEMP/gh-actions-lock"
+          echo "f9da98f2a6e9e0ae77deadf9a2319a8a86bb002b541cc3203b247cc59fb04842  $RUNNER_TEMP/gh-actions-lock" | sha256sum --check --strict
           chmod +x "$RUNNER_TEMP/gh-actions-lock"
           "$RUNNER_TEMP/gh-actions-lock" --verify-local
 
diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc
index 4b5741a..ea79cce 100644
--- a/PROOF-STATUS.adoc
+++ b/PROOF-STATUS.adoc
@@ -26,9 +26,9 @@ removed (the ABI proof obligations are owned by `+typed-wasm+`).
 |===
 |ID |Proof |Spans |Prover |File |Verified By
 |XP-1 |Pipeline information-loss = echo-types fibers |echo-types ↔
-affinescript ↔ typed-wasm |Agda (`+--safe --without-K+`)
+affinescript ↔ typed-wasm |Agda (`+--safe --without-K+`; historical; full-mode recheck pending)
 |`+verification/proofs/agda/EchoTyping.agda+`
-|`+agda Verification.agda+`
+|`+agda Verification.agda+` (legacy check; full-mode recheck pending)
 |===
 
 === Verification
@@ -37,7 +37,7 @@ affinescript ↔ typed-wasm |Agda (`+--safe --without-K+`)
 ----
 # Typecheck the cross-project Agda set (requires the echo-types library on the
 # Agda include path; see verification/proofs/agda/nextgen-typing.agda-lib)
-agda verification/proofs/agda/Verification.agda
+bash scripts/check-agda-verification.sh
 
 # Enforce the coordination boundary (no project code / non-allowlisted proofs)
 bash scripts/check-coordination-boundary.sh
@@ -54,3 +54,14 @@ proofs only |maintainer
 
 |2026-04-04 |Initial proof status tracking |Template
 |===
+
+=== 2026-11-01 proof-policy migration
+
+* The earlier XP-1 Agda result is preserved as historical evidence, **not**
+  presented as passing `--cubical-compatible`.
+* The current full-mode check is `bash scripts/check-agda-verification.sh`,
+  which invokes `agda --safe --without-K --cubical-compatible` and fails
+  if dependencies are missing or incompatible.
+* Coq/Rocq and Lean comparisons of XP-1 are **OPEN**. A proof transport,
+  statement comparison and independent kernel receipts have not been verified
+  in this change. See `docs/AGDA-RECONCILIATION.adoc`.
diff --git a/docs/AGDA-RECONCILIATION.adoc b/docs/AGDA-RECONCILIATION.adoc
new file mode 100644
index 0000000..c3b52b8
--- /dev/null
+++ b/docs/AGDA-RECONCILIATION.adoc
@@ -0,0 +1,33 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+= Agda cross-project proof recheck — coordination boundary
+:revdate: 2026-11-01
+
+Status: *RECHECK PENDING*. Do not treat the historical
+`agda Verification.agda` or `--safe --without-K` record as
+evidence of the stricter Cubical-compatible mode.
+
+The cross-project entrypoint is
+`verification/proofs/agda/Verification.agda`, which imports
+`EchoTyping.agda` and the external `echo-types` Agda library.
+Its dependency chain also includes the standard library and
+`absolute-zero`. Do not vendor or rewrite those libraries to force
+compatibility. Record the exact revisions and Agda/stdlib version
+used for any successful recheck.
+
+Use:
+
+[source,shell]
+----
+bash scripts/check-agda-verification.sh
+----
+
+This invokes `agda --safe --without-K --cubical-compatible`
+from the proper proof root. Failure or unavailable dependencies
+remain visible open obligations, not successes. A successful Agda
+check alone would prove the stated Agda fragment, *not* a
+cross-prover correspondence or end-to-end Wasm runtime refinement.
+
+Existing owning-family proof claims and CI remain with those
+families; coordination does not turn them into nextgen-typing code.
+The canonical policy is in `metadatastician/standards` and
+the theorem-level receipt inventory is planned in Mathesis.
diff --git a/scripts/check-agda-verification.sh b/scripts/check-agda-verification.sh
new file mode 100644
index 0000000..8af876a
--- /dev/null
+++ b/scripts/check-agda-verification.sh
@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Cross-project Agda proof gate (no implicit dependency download or skips).
+set -euo pipefail
+root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+if ! command -v agda >/dev/null 2>&1; then
+  echo "FATAL: Agda is missing; proof check is not optional." >&2
+  exit 1
+fi
+cd "$root/verification/proofs/agda"
+agda --version
+# The .agda-lib requires both standard-library and echo-types; echo-types
+# in turn requires absolute-zero. If imports are unavailable/incompatible,
+# this command fails visibly instead of fabricating a proof receipt.
+agda --safe --without-K --cubical-compatible Verification.agda