From bc8d4a3569959db652d9b977587806d847d571aa Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:05:19 +0000
Subject: [PATCH 01/12] docs(proofs): inventory Agda migration without
 overclaiming in nextgen-typing

---
 docs/AGDA-RECONCILIATION.adoc | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 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.

From b98f9feb59e29172d8f9b0b3cc525bf351cd205a Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:05:33 +0000
Subject: [PATCH 02/12] proofs(agda): add fail-closed full-policy cross-project
 checker

---
 scripts/check-agda-verification.sh | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 scripts/check-agda-verification.sh

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

From 741d075a9965b43ce44f67e15d9e441de5580b02 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:05:45 +0000
Subject: [PATCH 03/12] docs(proofs): mark Echo Agda and cross-prover
 reconciliation awaiting full policy check

---
 PROOF-STATUS.adoc | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

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`.

From 67a6cbc699eb591916d7951cebbd05bc2c046be8 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:09:01 +0000
Subject: [PATCH 04/12] ci(proofs): pin Echo and Absolute Zero for full-mode
 Agda check

---
 .github/workflows/agda-cross-project.yml | 66 ++++++++++++++++++++++++
 1 file changed, 66 insertions(+)
 create mode 100644 .github/workflows/agda-cross-project.yml

diff --git a/.github/workflows/agda-cross-project.yml b/.github/workflows/agda-cross-project.yml
new file mode 100644
index 0000000..ec8644f
--- /dev/null
+++ b/.github/workflows/agda-cross-project.yml
@@ -0,0 +1,66 @@
+# 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: 25
+    steps:
+      - name: Checkout
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: Install Agda and standard library
+        run: |
+          set -euo pipefail
+          sudo apt-get update -qq
+          sudo apt-get install -y --no-install-recommends agda agda-stdlib
+          agda --version
+
+      - 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
+          stdlib="$(find /usr/share -name standard-library.agda-lib -print -quit)"
+          test -n "$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

From ede073a3a68ee8518b64f3f415ce954193323642 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:25:39 +0000
Subject: [PATCH 05/12] ci(agda): register distro standard-library explicitly
 from installed package contents

---
 .github/workflows/agda-cross-project.yml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/agda-cross-project.yml b/.github/workflows/agda-cross-project.yml
index ec8644f..7b28900 100644
--- a/.github/workflows/agda-cross-project.yml
+++ b/.github/workflows/agda-cross-project.yml
@@ -52,8 +52,13 @@ jobs:
       - name: Register exact proof library revisions
         run: |
           set -euo pipefail
-          stdlib="$(find /usr/share -name standard-library.agda-lib -print -quit)"
-          test -n "$stdlib"
+          # Ubuntu's agda-stdlib package supplies sources but may not ship
+          # a discoverable .agda-lib descriptor. Use dpkg's file manifest
+          # to locate its root, then register a descriptor explicitly.
+          stdlib_root="$(dpkg -L agda-stdlib | sed -n 's#\\(.*\\)/Data/Nat\\.agda$#\\1#p' | head -n 1)"
+          test -n "$stdlib_root" && test -f "$stdlib_root/Data/Nat.agda"
+          stdlib="$RUNNER_TEMP/standard-library.agda-lib"
+          printf 'name: standard-library\\ninclude: %s\\n' "$stdlib_root" > "$stdlib"
           mkdir -p "$HOME/.agda"
           printf '%s\n' \
             "$stdlib" \

From 2184b148be81d5a5e243704bce80c345c7cdc137 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:26:00 +0000
Subject: [PATCH 06/12] fix(ci): correct Agda library descriptor registration
 shell quoting

---
 .github/workflows/agda-cross-project.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/agda-cross-project.yml b/.github/workflows/agda-cross-project.yml
index 7b28900..8a7e010 100644
--- a/.github/workflows/agda-cross-project.yml
+++ b/.github/workflows/agda-cross-project.yml
@@ -55,10 +55,10 @@ jobs:
           # Ubuntu's agda-stdlib package supplies sources but may not ship
           # a discoverable .agda-lib descriptor. Use dpkg's file manifest
           # to locate its root, then register a descriptor explicitly.
-          stdlib_root="$(dpkg -L agda-stdlib | sed -n 's#\\(.*\\)/Data/Nat\\.agda$#\\1#p' | head -n 1)"
+          stdlib_root="$(dpkg -L agda-stdlib | sed -n 's@/Data/Nat[.]agda$@@p' | head -n 1)"
           test -n "$stdlib_root" && test -f "$stdlib_root/Data/Nat.agda"
           stdlib="$RUNNER_TEMP/standard-library.agda-lib"
-          printf 'name: standard-library\\ninclude: %s\\n' "$stdlib_root" > "$stdlib"
+          printf 'name: standard-library\ninclude: %s\n' "$stdlib_root" > "$stdlib"
           mkdir -p "$HOME/.agda"
           printf '%s\n' \
             "$stdlib" \

From 2f72dbbc05e9c3e8ccd51978d955e97029227c96 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:29:13 +0000
Subject: [PATCH 07/12] ci(agda): use writable standard-library copy for Agda
 interface files

---
 .github/workflows/agda-cross-project.yml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/.github/workflows/agda-cross-project.yml b/.github/workflows/agda-cross-project.yml
index 8a7e010..c2a1dd4 100644
--- a/.github/workflows/agda-cross-project.yml
+++ b/.github/workflows/agda-cross-project.yml
@@ -57,6 +57,11 @@ jobs:
           # to locate its root, then register a descriptor explicitly.
           stdlib_root="$(dpkg -L agda-stdlib | sed -n 's@/Data/Nat[.]agda$@@p' | head -n 1)"
           test -n "$stdlib_root" && test -f "$stdlib_root/Data/Nat.agda"
+          # Agda 2.6.x writes .agdai interfaces beside imported sources.
+          # Distro /usr/share is read-only to CI's runner user; copy the
+          # pinned distro library to a writable temp tree, never sudo agda.
+          cp -a "$stdlib_root" "$RUNNER_TEMP/agda-stdlib-writable"
+          stdlib_root="$RUNNER_TEMP/agda-stdlib-writable"
           stdlib="$RUNNER_TEMP/standard-library.agda-lib"
           printf 'name: standard-library\ninclude: %s\n' "$stdlib_root" > "$stdlib"
           mkdir -p "$HOME/.agda"

From 99b753300a2ed3d5e3fa1acf42feb1a98de2c2d9 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:32:27 +0000
Subject: [PATCH 08/12] ci(agda): pin compatible Agda 2.7.0.1 and stdlib 2.1.1
 for Echo proofs

---
 .github/workflows/agda-cross-project.yml | 35 ++++++++++++------------
 1 file changed, 18 insertions(+), 17 deletions(-)

diff --git a/.github/workflows/agda-cross-project.yml b/.github/workflows/agda-cross-project.yml
index c2a1dd4..8cbbd7a 100644
--- a/.github/workflows/agda-cross-project.yml
+++ b/.github/workflows/agda-cross-project.yml
@@ -26,19 +26,29 @@ concurrency:
 jobs:
   typecheck:
     runs-on: ubuntu-24.04
-    timeout-minutes: 25
+    timeout-minutes: 45
     steps:
       - name: Checkout
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           persist-credentials: false
 
-      - name: Install Agda and standard library
+      - name: Setup Haskell for pinned Agda
+        uses: haskell-actions/setup@v2.12.1
+        with:
+          ghc-version: '9.6'
+          cabal-version: '3.10'
+
+      - name: Install Agda 2.7.0.1 and compatible stdlib 2.1.1
         run: |
           set -euo pipefail
-          sudo apt-get update -qq
-          sudo apt-get install -y --no-install-recommends agda agda-stdlib
-          agda --version
+          cabal update
+          cabal install Agda-2.7.0.1 --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: |
@@ -52,18 +62,9 @@ jobs:
       - name: Register exact proof library revisions
         run: |
           set -euo pipefail
-          # Ubuntu's agda-stdlib package supplies sources but may not ship
-          # a discoverable .agda-lib descriptor. Use dpkg's file manifest
-          # to locate its root, then register a descriptor explicitly.
-          stdlib_root="$(dpkg -L agda-stdlib | sed -n 's@/Data/Nat[.]agda$@@p' | head -n 1)"
-          test -n "$stdlib_root" && test -f "$stdlib_root/Data/Nat.agda"
-          # Agda 2.6.x writes .agdai interfaces beside imported sources.
-          # Distro /usr/share is read-only to CI's runner user; copy the
-          # pinned distro library to a writable temp tree, never sudo agda.
-          cp -a "$stdlib_root" "$RUNNER_TEMP/agda-stdlib-writable"
-          stdlib_root="$RUNNER_TEMP/agda-stdlib-writable"
-          stdlib="$RUNNER_TEMP/standard-library.agda-lib"
-          printf 'name: standard-library\ninclude: %s\n' "$stdlib_root" > "$stdlib"
+          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" \

From 8206069d85709e5d152a095b104bd3ecaa779b05 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:33:05 +0000
Subject: [PATCH 09/12] ci(agda): provision GHC/Cabal without extra marketplace
 action

---
 .github/workflows/agda-cross-project.yml | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/agda-cross-project.yml b/.github/workflows/agda-cross-project.yml
index 8cbbd7a..0251bfe 100644
--- a/.github/workflows/agda-cross-project.yml
+++ b/.github/workflows/agda-cross-project.yml
@@ -33,11 +33,15 @@ jobs:
         with:
           persist-credentials: false
 
-      - name: Setup Haskell for pinned Agda
-        uses: haskell-actions/setup@v2.12.1
-        with:
-          ghc-version: '9.6'
-          cabal-version: '3.10'
+      # 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
+          ghc --version
+          cabal --version
 
       - name: Install Agda 2.7.0.1 and compatible stdlib 2.1.1
         run: |

From 0cebe9edbf2cda433bc5fcbb2775c20924d93781 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:34:34 +0000
Subject: [PATCH 10/12] ci(lock): register pinned Agda workflow checkout in
 v0.0.3 actions lock

---
 .github/workflows/actions.lock | 7 +++++++
 1 file changed, 7 insertions(+)

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'

From ed9ee686b5a41db363b64dc52a8d10583dd4af12 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:36:28 +0000
Subject: [PATCH 11/12] ci(agda): force compatible distro GHC for pinned Agda
 2.7.0.1

---
 .github/workflows/agda-cross-project.yml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/agda-cross-project.yml b/.github/workflows/agda-cross-project.yml
index 0251bfe..530c1a7 100644
--- a/.github/workflows/agda-cross-project.yml
+++ b/.github/workflows/agda-cross-project.yml
@@ -40,14 +40,17 @@ jobs:
           set -euo pipefail
           sudo apt-get update -qq
           sudo apt-get install -y --no-install-recommends ghc cabal-install
-          ghc --version
+          # 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 --overwrite-policy=always
+          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

From 6a0400962587bad3451dba204682ae8493097865 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sun, 1 Nov 2026 01:49:30 +0000
Subject: [PATCH 12/12] ci(workflows): pin actions-lock v0.4.0 for v0.0.3
 manifest verification

---
 .github/workflows/workflow-linter.yml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

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