diff --git a/.github/workflows/boj-build.yml b/.github/workflows/boj-build.yml
deleted file mode 100644
index 9251f3a0..00000000
--- a/.github/workflows/boj-build.yml
+++ /dev/null
@@ -1,31 +0,0 @@
-# This workflow is managed by gh actions-lock.
-# SPDX-License-Identifier: MPL-2.0
-# This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
-# This workflow is managed by gh actions-lock.
-name: BoJ Server Build Trigger
-on:
-  push:
-    branches: [main, master]
-  workflow_dispatch:
-
-# Cause-B mitigation (#77): de-duplicate stacked BoJ build triggers.
-# cancel-in-progress is false so an in-flight dispatch always completes.
-concurrency:
-  group: ${{ github.workflow }}-${{ github.ref }}
-  cancel-in-progress: false
-
-jobs:
-  trigger-boj:
-    runs-on: ubuntu-latest
-    timeout-minutes: 10
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v7.0.1
-      - name: Trigger BoJ Server (Casket/ssg-mcp)
-        run: |
-          # Send a secure trigger to boj-server to build this repository
-          curl -X POST "http://boj-server.local:7700/cartridges/ssg-mcp/invoke"             -H "Content-Type: application/json"             -d "{\"repo\": \"${{ github.repository }}\", \"branch\": \"${{ github.ref_name }}\", \"engine\": \"casket\\"}"}
-        continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-permissions:
-  contents: read
diff --git a/.github/workflows/chapel-ci.yml b/.github/workflows/chapel-ci.yml
index abfeff2c..74f2b8c4 100644
--- a/.github/workflows/chapel-ci.yml
+++ b/.github/workflows/chapel-ci.yml
@@ -141,10 +141,10 @@ jobs:
           path: src/zig_ffi/zig-out/lib/
 
   # Job 3: Build Rust with chapel feature (links against Zig FFI stubs).
-  # Marked continue-on-error: true alongside its needed dependency zig-ffi
-  # (#133) — when the upstream Zig FFI build is allowed to fail, this job's
-  # "Download FFI library" step has no artifact to consume and red-fires.
-  # Re-enable strict gating once #133's Chapel + FFI rehabilitation lands.
+  # Blocking since the CI-4 ruling (#416). It was allow-fail while its
+  # dependency zig-ffi was; zig-ffi has been strict since #133 closed, and
+  # this job passed on main after #455 (run 42100322359) and on every PR run
+  # checked up to 2026-11-09.
   rust-chapel-feature:
     name: Rust Build with Chapel Feature
     runs-on: ubuntu-22.04
@@ -152,7 +152,6 @@ jobs:
     needs: zig-ffi
     env:
       ECHIDNA_CHAPEL_EXPECT_MODE: stubs
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
     steps:
       - uses: actions/checkout@v7.0.1
 
@@ -180,16 +179,19 @@ jobs:
   #
   # Cargo is the final static consumer: Zig's archive intentionally leaves
   # chapel_* references for libechidna_chapel.a + the compiler's runtime.
-  # No PIC rebuild is needed for this executable link. The existing #416
-  # waiver is unchanged; promotion requires the exact-source hosted result.
+  # No PIC rebuild is needed for this executable link.
+  #
+  # Blocking since the CI-4 ruling (#416). The real link landed with #455
+  # (build.rs, build_support/chapel.rs), and this job passed on main
+  # (run 42100322359, job 127501960139) and on every PR run checked up to
+  # 2026-11-09. It also consumes chapel-build's chapel-lib artifact.
   rust-chapel-real:
-    name: Rust Build — Real Chapel Library (allow-fail, L2.3+ gate)
+    name: Rust Build — Real Chapel Library
     runs-on: ubuntu-22.04
     timeout-minutes: 30
     needs: [chapel-build, zig-ffi]
     env:
       ECHIDNA_CHAPEL_EXPECT_MODE: real
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
     steps:
       - uses: actions/checkout@v7.0.1
 
diff --git a/.github/workflows/container-ci.yml b/.github/workflows/container-ci.yml
index 8cc44c81..007020c4 100644
--- a/.github/workflows/container-ci.yml
+++ b/.github/workflows/container-ci.yml
@@ -6,12 +6,23 @@
 #
 # container-ci.yml — Container build verification.
 #
-# Two jobs:
-#   container-build   — builds the minimal ECHIDNA image on every PR/push;
-#                       hard gate.
-#   tier3-container   — builds each Wave-3 prover image weekly (Sunday 06:00 UTC)
-#                       and on any change to the .containerization/** tree;
-#                       allow-fail per image (proprietary builds excluded).
+# Jobs, all blocking:
+#   container-build         — builds and verifies the minimal ECHIDNA image.
+#   container-rebuild       — builds the same image again on an independent
+#                             runner.
+#   container-reproducible  — requires both builds to have the same image ID.
+#                             This is the reproducibility check that replaced
+#                             the T1 Guix manifest job (owner ruling, CI-4):
+#                             the Containerfile is the reproducibility path.
+#   tier3-container         — builds each Wave-3 prover image weekly (Sunday
+#                             06:00 UTC); proprietary builds excluded.
+#
+# Both minimal builds use --no-cache and --timestamp 0, so creation times
+# and file mtimes cannot make two builds of the same inputs differ. A
+# mismatch means an input floats (an unpinned package, a download without
+# a digest, a non-deterministic build step). The compare job prints the
+# layer digests of both builds, and the deepest paths whose digests differ
+# (each build prints a per-path fingerprint, scripts/ci/fs-fingerprint.sh).
 
 name: Container Build Verification
 
@@ -24,6 +35,15 @@ on:
     paths:
       - 'Containerfile'
       - 'scripts/ci/install-lean.sh'
+      - 'scripts/ci/fs-fingerprint.sh'
+      - 'scripts/ci/fs-fingerprint-drift.sh'
+      - 'scripts/ci/test-fs-fingerprint.sh'
+      # Everything the Containerfile copies into the image (lines 26-42).
+      - 'build.rs'
+      - 'build_support/**'
+      - 'crates/**'
+      - 'benches/**'
+      - 'src/interfaces/**'
       - '.containerization/**'
       - 'Cargo.toml'
       - 'Cargo.lock'
@@ -33,6 +53,15 @@ on:
     paths:
       - 'Containerfile'
       - 'scripts/ci/install-lean.sh'
+      - 'scripts/ci/fs-fingerprint.sh'
+      - 'scripts/ci/fs-fingerprint-drift.sh'
+      - 'scripts/ci/test-fs-fingerprint.sh'
+      # Everything the Containerfile copies into the image (lines 26-42).
+      - 'build.rs'
+      - 'build_support/**'
+      - 'crates/**'
+      - 'benches/**'
+      - 'src/interfaces/**'
       - '.containerization/**'
       - 'Cargo.toml'
       - 'Cargo.lock'
@@ -43,6 +72,7 @@ on:
     # Distinct from live-provers.yml Tier-3 run (Sunday 05:00 UTC)
     # so the container build does not race the live-prover tests.
     - cron: '0 6 * * 0'
+  workflow_dispatch:
 
 # Cause-B mitigation (#77): de-duplicate superseded builds on the same
 # ref. cancel-in-progress is false so an in-flight image build/publish
@@ -60,11 +90,19 @@ jobs:
     name: Build & verify container image
     runs-on: ubuntu-latest
     timeout-minutes: 90
+    outputs:
+      image-id: ${{ steps.identity.outputs.image-id }}
+      layers: ${{ steps.identity.outputs.layers }}
 
     steps:
       - name: Checkout
         uses: actions/checkout@v7.0.1
 
+      # The fingerprint and drift scripts are exercised on every run, not only
+      # when two builds differ.
+      - name: Test filesystem fingerprints
+        run: bash scripts/ci/test-fs-fingerprint.sh
+
       - name: Install Podman
         run: |
           sudo apt-get update -q
@@ -76,8 +114,31 @@ jobs:
             -f Containerfile \
             -t echidna:ci-test \
             --no-cache \
+            --timestamp 0 \
             .
 
+      - name: Record image identity
+        id: identity
+        run: |
+          set -euo pipefail
+          echo "image-id=$(podman image inspect echidna:ci-test --format '{{.Id}}')" >> "$GITHUB_OUTPUT"
+          echo "layers=$(podman image inspect echidna:ci-test --format '{{json .RootFS.Layers}}')" >> "$GITHUB_OUTPUT"
+
+      # Per-path digests of the image filesystem, printed between markers so
+      # container-reproducible can name the drifting paths, not only the layer.
+      - name: Fingerprint the image filesystem
+        run: |
+          set -euo pipefail
+          cid=$(podman create echidna:ci-test)
+          podman export "$cid" | bash scripts/ci/fs-fingerprint.sh 12 > "$RUNNER_TEMP/fs-fingerprint"
+          podman rm "$cid" >/dev/null
+          echo "fs-fingerprint: $(wc -l < "$RUNNER_TEMP/fs-fingerprint") paths"
+          echo "::group::fs-fingerprint (depth 12)"
+          echo "FS-FINGERPRINT-BEGIN"
+          cat "$RUNNER_TEMP/fs-fingerprint"
+          echo "FS-FINGERPRINT-END"
+          echo "::endgroup::"
+
       - name: Verify image metadata
         run: |
           echo "=== Image labels ==="
@@ -105,11 +166,120 @@ jobs:
         if: always()
         run: podman rmi echidna:ci-test 2>/dev/null || true
 
-  # ── Job 2: Wave-3 Tier-3 prover images — weekly, allow-fail per image ─────
+  # ── Containerfile reproducibility: an independent rebuild ─────────────────
+  container-rebuild:
+    name: Rebuild container image (independent runner)
+    runs-on: ubuntu-latest
+    timeout-minutes: 90
+    outputs:
+      image-id: ${{ steps.identity.outputs.image-id }}
+      layers: ${{ steps.identity.outputs.layers }}
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v7.0.1
+
+      - name: Install Podman
+        run: |
+          sudo apt-get update -q
+          sudo apt-get install -y -q podman
+
+      - name: Rebuild minimal container image
+        run: |
+          podman build \
+            -f Containerfile \
+            -t echidna:ci-rebuild \
+            --no-cache \
+            --timestamp 0 \
+            .
+
+      - name: Record image identity
+        id: identity
+        run: |
+          set -euo pipefail
+          echo "image-id=$(podman image inspect echidna:ci-rebuild --format '{{.Id}}')" >> "$GITHUB_OUTPUT"
+          echo "layers=$(podman image inspect echidna:ci-rebuild --format '{{json .RootFS.Layers}}')" >> "$GITHUB_OUTPUT"
+
+      # Per-path digests of the image filesystem, printed between markers so
+      # container-reproducible can name the drifting paths, not only the layer.
+      - name: Fingerprint the image filesystem
+        run: |
+          set -euo pipefail
+          cid=$(podman create echidna:ci-rebuild)
+          podman export "$cid" | bash scripts/ci/fs-fingerprint.sh 12 > "$RUNNER_TEMP/fs-fingerprint"
+          podman rm "$cid" >/dev/null
+          echo "fs-fingerprint: $(wc -l < "$RUNNER_TEMP/fs-fingerprint") paths"
+          echo "::group::fs-fingerprint (depth 12)"
+          echo "FS-FINGERPRINT-BEGIN"
+          cat "$RUNNER_TEMP/fs-fingerprint"
+          echo "FS-FINGERPRINT-END"
+          echo "::endgroup::"
+
+  container-reproducible:
+    name: Containerfile reproducibility (same image ID twice)
+    runs-on: ubuntu-latest
+    timeout-minutes: 10
+    needs: [container-build, container-rebuild]
+    permissions:
+      actions: read     # read the two build jobs' logs for their fs-fingerprints
+      contents: read
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v7.0.1
+
+      - name: Compare the two builds
+        env:
+          GH_TOKEN: ${{ github.token }}
+          ID_A: ${{ needs.container-build.outputs.image-id }}
+          ID_B: ${{ needs.container-rebuild.outputs.image-id }}
+          LAYERS_A: ${{ needs.container-build.outputs.layers }}
+          LAYERS_B: ${{ needs.container-rebuild.outputs.layers }}
+        run: |
+          set -euo pipefail
+          if [ -z "$ID_A" ] || [ -z "$ID_B" ]; then echo "::error::a build reported no image ID"; exit 1; fi
+          {
+            echo "## Containerfile reproducibility"
+            echo "build:   $ID_A"
+            echo "rebuild: $ID_B"
+          } >> "$GITHUB_STEP_SUMMARY"
+          if [ "$ID_A" = "$ID_B" ]; then
+            echo "OK: two independent --no-cache --timestamp 0 builds gave image $ID_A"
+            exit 0
+          fi
+          echo "::error::The Containerfile is not reproducible: two builds of the same commit gave $ID_A and $ID_B."
+          paste <(jq -r '.[]' <<<"$LAYERS_A") <(jq -r '.[]' <<<"$LAYERS_B") \
+            | awk -F '\t' '{ printf "layer %d: %s %s %s\n", NR, ($1 == $2 ? "same" : "DIFFERS"), $1, $2 }' \
+            | tee -a "$GITHUB_STEP_SUMMARY"
+          # Name the drift: each build job printed per-path digests of its
+          # image between markers (scripts/ci/fs-fingerprint.sh).
+          fingerprint() {
+            local id
+            id=$(gh api "repos/$GITHUB_REPOSITORY/actions/runs/$GITHUB_RUN_ID/attempts/$GITHUB_RUN_ATTEMPT/jobs" \
+                   --paginate --jq ".jobs[] | select(.name == \"$1\") | .id" | head -n 1)
+            [ -n "$id" ] || { echo "::warning::no job named '$1' in this run attempt"; return 1; }
+            gh api "repos/$GITHUB_REPOSITORY/actions/jobs/$id/logs" \
+              | sed -E 's/^[0-9]{4}-[0-9]{2}-[0-9]{2}T[0-9:.]+Z //' \
+              | sed -n '/^FS-FINGERPRINT-BEGIN$/,/^FS-FINGERPRINT-END$/p' \
+              | grep -E '^[0-9a-f]{64}  '
+          }
+          if fingerprint "Build & verify container image" > "$RUNNER_TEMP/fp-a" \
+             && fingerprint "Rebuild container image (independent runner)" > "$RUNNER_TEMP/fp-b"; then
+            {
+              echo "### Paths that differ between the two builds (deepest only)"
+              echo '```'
+              bash scripts/ci/fs-fingerprint-drift.sh "$RUNNER_TEMP/fp-a" "$RUNNER_TEMP/fp-b" | head -n 200
+              echo '```'
+            } | tee -a "$GITHUB_STEP_SUMMARY"
+          else
+            echo "::warning::could not read both fs-fingerprints; only the layer comparison is available"
+          fi
+          exit 1
+
+  # ── Wave-3 Tier-3 prover images — weekly, blocking per image ──────────────
   #
-  # Runs on the weekly schedule and whenever any .containerization/** file
-  # changes.  Each prover builds in its own matrix cell; allow-fail is set
-  # at cell level so one broken prover does not mask the others.
+  # Runs on the weekly schedule. Each prover builds in its own matrix cell
+  # (fail-fast off), so one broken prover does not mask the others. Blocking
+  # since the CI-4 ruling (#416): the scheduled run on main of 2026-11-08
+  # (42453284210) passed all eight cells, stub-sentinel detection included.
   #
   # Imandra is excluded: it is proprietary and requires a licence token not
   # available in public CI.
@@ -117,12 +287,9 @@ jobs:
     name: Tier-3 / ${{ matrix.prover }}
     runs-on: ubuntu-latest
     timeout-minutes: 90
-    # Run on schedule or when the .containerization tree changes on main.
-    # Not a merge gate — these are informational weekly builds.
-    if: >-
-      github.event_name == 'schedule' ||
-      (github.event_name == 'push' && contains(github.event.head_commit.modified, '.containerization/'))
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
+    # Weekly and on manual dispatch. A red cell is a real failure, but these
+    # builds are too slow to gate every PR.
+    if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
     strategy:
       fail-fast: false
       matrix:
diff --git a/.github/workflows/live-provers.yml b/.github/workflows/live-provers.yml
index b5ed9ea2..0bd08a9c 100644
--- a/.github/workflows/live-provers.yml
+++ b/.github/workflows/live-provers.yml
@@ -6,18 +6,21 @@
 # Exercises real prover binaries against canonical micro-goals. Complements
 # rust-ci.yml (which runs mock tests on every PR) with live-subprocess coverage.
 #
-# Tiering (matches ~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md + manifests/live-provers.scm):
+# Tiering (matches ~/Desktop/ECHIDNA-PRODUCTION-WIRING-PLAN.md):
 #   T1 — trivial    — every PR + push to main
 #   T2 — build      — nightly
 #   T3 — container  — weekly
-#   T4 — niche      — quarterly, allow-fail
 #
-# Reproducibility paths (both tried; at least one must succeed):
-#   1. Guix manifest (PRIMARY, per project CLAUDE.md): manifests/live-provers.scm
-#   2. apt-get (expedient bootstrap for T1 only):       jobs below
+# Every job here is blocking: the allow-fail units were made blocking or
+# removed under the CI-4 ruling (2026-11-05, #416). Removed: the quarterly T4
+# jobs (a TODO announcement, and a GPUVerify/Faial check that never
+# provisioned either binary) and the T1 Guix manifest check.
 #
-# (Guix flake removed 2026-06-01 per estate-wide guix-deprecation directive;
-# Guix is the sole reproducible-build primary.)
+# Reproducibility: the Containerfile is the reproducibility path (owner
+# ruling, CI-4). container-ci.yml rebuilds the minimal image on a second,
+# independent runner and requires the same image ID. The jobs below
+# provision provers with apt and with digest- or version-pinned upstream
+# releases.
 
 name: Live Provers
 
@@ -29,11 +32,10 @@ on:
   schedule:
     - cron: '0 3 * * *'    # Tier-2 nightly at 03:00 UTC
     - cron: '0 5 * * 0'    # Tier-3 weekly  Sunday 05:00 UTC
-    - cron: '0 6 1 */3 *'  # Tier-4 quarterly 1st of Jan/Apr/Jul/Oct 06:00 UTC
   workflow_dispatch:
     inputs:
       tier:
-        description: 'Which tier to run (1|2|3|4|all)'
+        description: 'Which tier to run (1|2|3|all)'
         required: false
         default: '1'
 
@@ -140,40 +142,6 @@ jobs:
           LIVE_PROVER: ${{ matrix.backend }}
         run: bash scripts/ci/run-live-prover.sh "$LIVE_PROVER"
 
-  # ============================================================================
-  # Resolve the explicitly packaged Guix subset. This is not live-prover
-  # execution evidence and does not cover the externally provisioned backends.
-  # ============================================================================
-  tier1-guix-reproducibility:
-    name: T1 Guix manifest check
-    if: github.event_name != 'schedule' || github.event.schedule == '0 3 * * *'
-    # Ubuntu 26.04 removed the guix APT package. Noble has this audited version.
-    runs-on: ubuntu-24.04
-    timeout-minutes: 20
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v7.0.1
-      - name: Install Guix
-        run: |
-          set -euo pipefail
-          trap 'echo "::error::Guix setup failed; manifest check NOT RUN"; exit 2' ERR
-          sudo apt-get update -qq
-          sudo apt-get install -y --no-install-recommends guix=1.4.0-6build1
-          sudo systemctl start guix-daemon
-          guix --version
-      - name: Resolve packaged manifest (not a live-prover test)
-        run: |
-          set -euo pipefail
-          {
-            echo '## Guix manifest scope'
-            echo
-            echo 'This job resolves the Guix-packaged subset; it does not build or run provers.'
-            echo 'Guix coverage for cvc5, alt-ergo, vampire, eprover, spass, chuffed, Idris2 and Isabelle is UNKNOWN.'
-            echo 'Their separate live-prover jobs must supply execution evidence; this job cannot satisfy it.'
-            echo 'See manifests/live-provers.scm for the package boundary.'
-          } >> "$GITHUB_STEP_SUMMARY"
-          guix package --manifest=manifests/live-provers.scm --dry-run --no-substitutes
-
   # ============================================================================
   # Tier 2 — nightly.  Larger build-from-source provers.
   # ============================================================================
@@ -205,8 +173,11 @@ jobs:
           toolchain: stable
       - name: Cache Cargo
         uses: Swatinem/rust-cache@v2.9.3
-      - name: Provision ${{ matrix.backend }} (best-effort via apt / upstream release)
-        continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
+      # Blocking since the CI-4 ruling (#416). In the nightly runs up to
+      # 2026-11-09 only the Isabelle download failed in this step; Isabelle
+      # now installs through scripts/ci/install-isabelle.sh, so any
+      # provisioning failure here is a real one.
+      - name: Provision ${{ matrix.backend }} (apt / pinned upstream release)
         run: |
           set -euo pipefail
           readonly https_protocol='=https'
@@ -241,17 +212,11 @@ jobs:
               echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
               ;;
             isabelle)
-              # Isabelle2024 tarball (~500MB); nightly only.
-              # --retry 3 + --max-time 600 guard the large download.
-              # find locates the binary regardless of extracted dir name,
-              # so the symlink survives a future Isabelle2025 release.
-              curl --proto "$https_protocol" --proto-redir "$https_protocol" -fsSL --max-time 600 --retry 3 --retry-delay 15 \
-                -o /tmp/isabelle.tar.gz \
-                https://isabelle.in.tum.de/dist/Isabelle2024_linux.tar.gz
-              sudo mkdir -p /opt/isabelle
-              sudo tar xzf /tmp/isabelle.tar.gz -C /opt/isabelle
-              ISABELLE_BIN="$(find /opt/isabelle -type f -name isabelle | head -n 1)"
-              [ -n "$ISABELLE_BIN" ] && sudo ln -sf "$ISABELLE_BIN" /usr/local/bin/isabelle
+              # Pinned release and SHA-256, https-only mirrors (the upstream
+              # dist/ path redirected to http:// and reset connections from
+              # hosted runners on the nightlies up to 2026-11-09). One
+              # installer serves this job and verification-proofs-cron.yml.
+              bash scripts/ci/install-isabelle.sh
               ;;
             why3)
               sudo apt-get install -y --fix-missing why3
@@ -320,16 +285,20 @@ jobs:
   #   A — live-provisioned today via apt / upstream tarball (tamarin, proverif,
   #       metamath, twelf, ortools).  Version-check runs, skip-if-absent.
   #   B — heavy-build deferred (hol4, acl2, scip) and proprietary (imandra).
-  #       Provisioning step emits a skip note; test step runs the suite with
-  #       continue-on-error so the matrix stays green and the binary's absence
-  #       is logged as SKIP by the suite's `which` probe.
+  #       Provisioning step emits a skip note, and the binary's absence is
+  #       logged as SKIP by the suite's `which` probe. Their containerised
+  #       builds are checked by container-ci.yml's tier3-container job.
+  #
+  # The job and its provisioning step are blocking since the CI-4 ruling
+  # (#416). On the weekly runs up to 2026-11-09 only proverif failed inside
+  # the provisioning step (no apt package on the runner image); it records
+  # NOT RUN in the step summary instead of failing, like twelf.
   # ============================================================================
   tier3:
     name: T3 / ${{ matrix.backend }}
     if: github.event_name == 'schedule' && github.event.schedule == '0 5 * * 0' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '3' || inputs.tier == 'all'))
     runs-on: ubuntu-latest
     timeout-minutes: 20
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
     strategy:
       fail-fast: false
       matrix:
@@ -352,8 +321,7 @@ jobs:
           toolchain: stable
       - name: Cache Cargo
         uses: Swatinem/rust-cache@v2.9.3
-      - name: Provision ${{ matrix.backend }} (best-effort)
-        continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
+      - name: Provision ${{ matrix.backend }}
         run: |
           set -euo pipefail
           readonly https_protocol='=https'
@@ -372,8 +340,15 @@ jobs:
               [ -n "$TAMARIN_BIN" ] && sudo ln -sf "$TAMARIN_BIN" /usr/local/bin/tamarin-prover
               ;;
             proverif)
-              # ProVerif is in the Ubuntu/Debian main repos.
-              sudo apt-get install -y proverif
+              # ProVerif had no apt package on ubuntu-latest in the weekly
+              # runs up to 2026-11-09 ("Unable to locate package"). Record
+              # that as NOT RUN rather than a pass; the containerised build
+              # in container-ci.yml (tier3-container) remains the check that
+              # ProVerif itself still builds.
+              sudo apt-get install -y proverif || {
+                echo "::warning::proverif: no apt package on this runner image; not installed, live test will SKIP."
+                echo "proverif: NOT RUN (no apt package on this runner image)" >> "$GITHUB_STEP_SUMMARY"
+              }
               ;;
             metamath)
               # metamath-exe is small; apt-installable on Ubuntu with build fallback.
@@ -387,8 +362,10 @@ jobs:
               ;;
             twelf)
               # Twelf is in Debian with SML/NJ; on Ubuntu it may live in universe.
-              sudo apt-get install -y twelf || \
+              sudo apt-get install -y twelf || {
                 echo "twelf unavailable via apt on this runner; test will SKIP."
+                echo "twelf: NOT RUN (no apt package on this runner image)" >> "$GITHUB_STEP_SUMMARY"
+              }
               ;;
             ortools)
               # Google OR-Tools ships prebuilt Linux tarballs.  The binary we
@@ -396,6 +373,7 @@ jobs:
               OR_URL="https://github.com/google/or-tools/releases/latest/download/or-tools_amd64_ubuntu-22.04_cpp_v9.11.4210.tar.gz"
               curl --proto "$https_protocol" --proto-redir "$https_protocol" -fsSL -o /tmp/ortools.tar.gz "$OR_URL" || {
                 echo "OR-Tools tarball unavailable at expected URL; test will SKIP."
+                echo "ortools: NOT RUN (release tarball unavailable)" >> "$GITHUB_STEP_SUMMARY"
                 exit 0
               }
               sudo mkdir -p /opt/ortools
@@ -438,78 +416,3 @@ jobs:
           esac
       - name: Run live test for ${{ matrix.backend }}
         run: cargo test --test live_prover_suite --features live-provers -- --nocapture ${{ matrix.backend }}
-
-  # ============================================================================
-  # Tier 4 — quarterly, best-effort / allow-fail.
-  # ============================================================================
-  tier4:
-    name: T4 niche provers
-    if: github.event_name == 'schedule' && github.event.schedule == '0 6 1 */3 *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '4' || inputs.tier == 'all'))
-    runs-on: ubuntu-latest
-    timeout-minutes: 20
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v7.0.1
-      - name: Announce Wave-4 TODO
-        run: |
-          echo "Tier-4 backends (Mizar, Nuprl, PVS, Minlog, Dedukti, Arend, KeY, Prism, UPPAAL,"
-          echo "ViPER, NuSMV, Spin, TLC, CBMC, Seahorn, dReal, Boogie, Kissat, Alloy) are"
-          echo "retained as mock-only unless a maintainer volunteers a Containerfile."
-
-  # ============================================================================
-  # Tier 4 GPU — quarterly, best-effort / allow-fail.
-  # GPUVerify and Faial require CUDA SDK or OpenCL runtime; provisioning is
-  # deferred to a developer workstation or GPU-capable CI runner.
-  # ============================================================================
-  tier4-gpu:
-    name: T4 / ${{ matrix.backend }}
-    if: github.event_name == 'schedule' && github.event.schedule == '0 6 1 */3 *' || (github.event_name == 'workflow_dispatch' && (inputs.tier == '4' || inputs.tier == 'all'))
-    runs-on: ubuntu-latest
-    timeout-minutes: 20
-    continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-    strategy:
-      fail-fast: false
-      matrix:
-        backend:
-          - gpuverify
-          - faial
-    steps:
-      - name: Checkout
-        uses: actions/checkout@v7.0.1
-      - name: Install Rust
-        uses: dtolnay/rust-toolchain@v1
-        with:
-          toolchain: stable
-      - name: Cache Cargo
-        uses: Swatinem/rust-cache@v2.9.3
-      - name: Provision ${{ matrix.backend }} (best-effort, CUDA/OpenCL required)
-        continue-on-error: true  # allow-fail: issue=#416 expires=2026-11-30
-        run: |
-          case "${{ matrix.backend }}" in
-            gpuverify)
-              echo "GPUVerify requires CUDA SDK + .NET; deferred to developer workstation."
-              echo "See: https://github.com/mc-imperial/gpuverify"
-              ;;
-            faial)
-              echo "Faial requires CUDA/OpenCL headers; install via: cargo install faial"
-              echo "See: https://github.com/elliotttate/faial"
-              ;;
-          esac
-      - name: Require selected live version check
-        env:
-          LIVE_PROVER: ${{ matrix.backend }}
-        run: bash scripts/ci/run-live-prover.sh "$LIVE_PROVER"
-      - name: Record selected GPU capability
-        if: always()
-        env:
-          LIVE_PROVER: ${{ matrix.backend }}
-          GPU_JOB_STATUS: ${{ job.status }}
-        run: |
-          {
-            echo "## Selected GPU backend: $LIVE_PROVER"
-            echo "Execution status: $GPU_JOB_STATUS"
-            echo 'Missing tools mean NOT RUN, never a passed version check.'
-            echo 'The temporary job-level allow-fail is issue #416, expires 2026-11-30.'
-            echo 'A passed version probe establishes executable identity, not proof correctness.'
-          } >> "$GITHUB_STEP_SUMMARY"
diff --git a/.github/workflows/verification-proofs-cron.yml b/.github/workflows/verification-proofs-cron.yml
index 226d254a..9a5e2a31 100644
--- a/.github/workflows/verification-proofs-cron.yml
+++ b/.github/workflows/verification-proofs-cron.yml
@@ -25,6 +25,7 @@ on:
   pull_request:
     paths:
       - 'proofs/isabelle/**'
+      - 'scripts/ci/install-isabelle.sh'
       - '.github/workflows/verification-proofs-cron.yml'
 
 concurrency:
@@ -43,17 +44,10 @@ jobs:
       - uses: actions/checkout@v7.0.1
 
       - name: Install Isabelle
-        run: |
-          set -euo pipefail
-          # Official Cambridge distribution mirror; immutable version and digest.
-          curl -fL --max-time 900 --retry 3 --retry-delay 15 \
-            -o /tmp/isabelle.tar.gz \
-            https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2025-2_linux.tar.gz
-          echo "a20a507bc7c1270d8be96a9f3fbec06345387789d2dc2c4d3df6260d47bfb33c  /tmp/isabelle.tar.gz" | sha256sum --check
-          sudo mkdir -p /opt/isabelle
-          sudo tar xzf /tmp/isabelle.tar.gz -C /opt/isabelle
-          sudo ln -sf /opt/isabelle/Isabelle2025-2/bin/isabelle /usr/local/bin/isabelle
-          isabelle version
+        # Pinned release, digest and https-only mirrors live in the script.
+        # The old inline URL used the mirror's current-release dist/ path,
+        # which returned 404 once that release was superseded (2026-11-09).
+        run: bash scripts/ci/install-isabelle.sh
 
       - name: Install just
         run: |
diff --git a/docs/decisions/2026-05-30-chapel-rehabilitation.adoc b/docs/decisions/2026-05-30-chapel-rehabilitation.adoc
index ecaac65f..ad394b2f 100644
--- a/docs/decisions/2026-05-30-chapel-rehabilitation.adoc
+++ b/docs/decisions/2026-05-30-chapel-rehabilitation.adoc
@@ -88,6 +88,9 @@ indicate a genuine regression. `+rust-chapel-real+` stays allow-fail
 because the Rust-side link of the full Chapel runtime is a different
 scope (gated on the PIC-runtime work above and on the static-archive
 integration in `+build.zig+`).
+_Superseded 2026-11-09:_ `+rust-chapel-real+` is blocking. The real link
+landed with #455 as a static link (see the update under *Negative* below);
+the PIC rebuild now concerns shared-library output only.
 
 === Rollout
 
@@ -104,6 +107,9 @@ recipes: `+chapel-build+`, `+chapel-smoke+`, `+chapel-test+`.
 Wave 2 (separate PR, after Wave 1 green-on-main for ≥7 days): - Rebuild
 Chapel from source with `+CHPL_LIB_PIC=pic+` runtime; revert the
 metalayer build to `+--dynamic+`; flip `+rust-chapel-real+` to strict.
+_Superseded 2026-11-09:_ `+rust-chapel-real+` was made strict without the
+PIC rebuild (static link, #455); the PIC rebuild remains relevant only for
+shared-library output.
 Recipe + tradeoffs:
 link:./2026-05-30-chapel-pic-rebuild.md[2026-05-30-chapel-pic-rebuild.adoc].
 CI flip deferred — the ~30 min source build dominates the chapel-ci
@@ -145,6 +151,11 @@ composable with the existing `+SoundnessPreservation+` proof.
 * Static-library distribution means the Rust-side link path
 (`+rust-chapel-real+`) remains allow-fail until the PIC-runtime CI image
 lands. Wave-2 work is non-trivial.
++
+_Update 2026-11-09._ The real link landed with #455 as a static link
+with Cargo as the final consumer (`+build.rs+`, `+build_support/chapel.rs+`),
+with no PIC rebuild. `+rust-chapel-real+` passed on main from then on and is
+blocking under the CI-4 ruling (#416), as is `+rust-chapel-feature+`.
 * `+chapel-ci.yml+`’s install step downloads a ~150 MB Chapel deb per
 run; this is unchanged from the prior state but matters more now that
 the job is strict (any apt mirror flake red-checks the workflow).
diff --git a/docs/handover/STATE.adoc b/docs/handover/STATE.adoc
index ed39e012..2cd0f96d 100644
--- a/docs/handover/STATE.adoc
+++ b/docs/handover/STATE.adoc
@@ -45,7 +45,9 @@ highest-leverage gap, surfaces real bugs mocks hide. Cap’n Proto next,
 since Chapel consumes those schemas.
 
 |D5 |*Live-prover CI cadence tiered* |T1 every PR, T2 nightly, T3
-weekly, T4 quarterly allow-fail.
+weekly. (The T4 quarterly allow-fail jobs and the T1 Guix manifest check
+were removed 2026-11-09 under the CI-4 ruling, #416; every remaining job
+is blocking.)
 
 |D6 |*No JSON emit on hot path* |Per `+feedback_no_json_emit_a2ml+`.
 Cap’n Proto replaces HTTP-JSON Rust↔Julia. Tool config stays
@@ -75,8 +77,9 @@ CI-unverified |`+9a4aeeb+`, `+6717b12+`
 OR-Tools, HOL4, ACL2, Twelf, Metamath). Needs per-backend Containerfiles
 (Podman). |*SCAFFOLD ONLY* — handover hints in STATE.a2ml |—
 
-|Wave-4 |Tier-4 quarterly, 19 backends. Retained as mock-only unless a
-maintainer volunteers. |*SCAFFOLD ONLY* |—
+|Wave-4 |Tier-4, 19 backends, mock-only. The quarterly CI placeholder jobs
+were removed 2026-11-09 (CI-4, #416); a backend returns to CI in a blocking
+job once it has a Containerfile. |*SCAFFOLD ONLY* |—
 |===
 
 Local verification of Wave-1 + Wave-2: *18/18 live tests pass* (13 real
@@ -133,8 +136,8 @@ Baseline smoke.
 FFI bridge. *Does not feed into dispatch* and *does not link real
 Chapel*; tests run against bundled stubs only.
 * `+.github/workflows/live-provers.yml+` — tiered workflow (T1 PR, T2
-nightly, T3 weekly, T4 quarterly). T1 + T2 matrices filled with real
-provisioning; T3 + T4 placeholder jobs.
+nightly, T3 weekly). T1 + T2 matrices filled with real provisioning. The
+T4 quarterly placeholder jobs were removed 2026-11-09 (CI-4, #416).
 * `+.github/workflows/agda-meta-checker.yml+` — formally-verified
 trust-pipeline properties.
 
diff --git a/docs/handover/TODO.adoc b/docs/handover/TODO.adoc
index 08d768b5..181c9f73 100644
--- a/docs/handover/TODO.adoc
+++ b/docs/handover/TODO.adoc
@@ -155,7 +155,11 @@ at-source. *#74 (proverif opam) resolved.* Imandra remains the only stub
 — genuinely proprietary, honestly fail-loud, kept by decision (real
 adapter + Idris2 ABI proofs retained). No stub-theatre.
 
-==== Wave-4 (Tier-4 quarterly, 19 backends, allow-fail placeholder)
+==== Wave-4 (Tier-4, 19 backends, mock-only)
+
+_The quarterly Tier-4 CI placeholder jobs were removed 2026-11-09 under the
+CI-4 ruling (#416): they announced a TODO and never provisioned a binary.
+A backend returns to CI in a blocking job once it has a Containerfile._
 
 Mizar, Nuprl, PVS, Minlog, Dedukti, Arend, KeY, Prism, UPPAAL, ViPER,
 NuSMV, Spin, TLC, CBMC, Seahorn, dReal, Boogie, Kissat, Alloy. Retain as
@@ -380,7 +384,8 @@ acceptance run.
 
 *P1 L3 finishers:* Wave-3 ✅ DONE & consolidated to one
 `+Containerfile.wave3+` (2026-05-18; see Wave-3 section above), Wave-4
-✅ (19 placeholder + rationale docs in STATE.a2ml). L3 P1 finisher work
+✅ (19 backends documented as mock-only in STATE.a2ml; the CI placeholder
+jobs were removed 2026-11-09, CI-4 #416). L3 P1 finisher work
 is complete; the L3→L1 hand-off remains gated only on the calendar/infra
 gate (Tier-1 green ≥7 days on main — blocked by main CI stuck
 `+queued/+`, infra-owned, not collapsible here).
diff --git a/manifests/live-provers.scm b/manifests/live-provers.scm
index 51d198cc..f63c548f 100644
--- a/manifests/live-provers.scm
+++ b/manifests/live-provers.scm
@@ -6,7 +6,11 @@
 ;; Purpose: resolve the subset packaged by GNU Guix 1.4.0 (the CI baseline).
 ;; This manifest is NOT a declaration that every live prover is packaged or
 ;; tested. Resolution does not prove that a prover ran or that a proof passed.
-;; Used by `.github/workflows/live-provers.yml` and local developers via:
+;; It has no CI consumer: the T1 Guix manifest check in live-provers.yml was
+;; retired 2026-11-09 under the CI-4 ruling (#416), and the Containerfile is
+;; the reproducibility path (container-ci.yml rebuilds the image on an
+;; independent runner and requires the same image ID). Local developers can
+;; still resolve it via:
 ;;
 ;;     guix package -m manifests/live-provers.scm --dry-run --no-substitutes
 ;;
@@ -18,7 +22,8 @@
 ;;   T1 — trivial (apt/Guix single-package)       — run on every PR
 ;;   T2 — build-from-source                       — run nightly
 ;;   T3 — container / special env                 — run weekly
-;;   T4 — niche / best-effort                     — run quarterly, allow-fail
+;;   T4 — niche / best-effort                     — no CI job (quarterly
+;;        allow-fail jobs retired 2026-11-09, CI-4 #416; mock-only)
 ;;
 ;; Policy (estate ruling 2026-05-18 + estate-wide nix-deprecation 2026-06-01):
 ;;   Guix is the PRIMARY (and only) package-management path declared here.
diff --git a/scripts/ci/check-allow-fail-expiry.sh b/scripts/ci/check-allow-fail-expiry.sh
index 9d96b8ee..aae13c38 100755
--- a/scripts/ci/check-allow-fail-expiry.sh
+++ b/scripts/ci/check-allow-fail-expiry.sh
@@ -19,6 +19,10 @@
 #
 # Usage: check-allow-fail-expiry.sh [--today YYYY-MM-DD] [--warn-days N] [DIR ...]
 #
+# The date defaults to FAKE_DATE when that is set (for example
+# `FAKE_DATE=2026-12-01 scripts/ci/check-allow-fail-expiry.sh`, the W0 exit
+# gate), otherwise to today in UTC. `--today` overrides both.
+#
 # Exit codes: 0 all units owned and in date, 1 a unit is unowned, undated,
 # or expired, 2 bad arguments.
 
@@ -31,9 +35,9 @@ dirs=()
 
 while [ $# -gt 0 ]; do
   case "$1" in
-    --today) [ $# -ge 2 ] || { echo "--today needs a value" >&2; exit 2; }; today="$2"; shift 2 ;;
+    --today) { [ $# -ge 2 ] && [ -n "$2" ]; } || { echo "--today needs a non-empty value" >&2; exit 2; }; today="$2"; shift 2 ;;
     --warn-days) [ $# -ge 2 ] || { echo "--warn-days needs a value" >&2; exit 2; }; warn_days="$2"; shift 2 ;;
-    -h|--help) sed -n '3,20p' "$0"; exit 0 ;;
+    -h|--help) sed -n '3,25p' "$0"; exit 0 ;;
     --) shift; dirs+=("$@"); break ;;
     -*) echo "unknown option: $1" >&2; exit 2 ;;
     *) dirs+=("$1"); shift ;;
@@ -44,7 +48,7 @@ if [ ${#dirs[@]} -eq 0 ]; then
   dirs=(.github/workflows)
 fi
 if [ -z "$today" ]; then
-  today=$(date +%F)
+  today=${FAKE_DATE:-$(date +%F)}
 fi
 if ! today_s=$(date -d "$today" +%s 2>/dev/null); then
   echo "invalid --today: $today" >&2
diff --git a/scripts/ci/fs-fingerprint-drift.sh b/scripts/ci/fs-fingerprint-drift.sh
new file mode 100755
index 00000000..62e33957
--- /dev/null
+++ b/scripts/ci/fs-fingerprint-drift.sh
@@ -0,0 +1,19 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# fs-fingerprint-drift.sh A B
+#
+# A and B are fs-fingerprint.sh outputs ("<sha256>  <path>" per line).
+# Prints the deepest paths whose digest differs or that exist on one side
+# only. An ancestor of a printed path is left out, since it differs only
+# because the path beneath it does.
+set -euo pipefail
+a=${1:?usage: fs-fingerprint-drift.sh A B}; b=${2:?usage: fs-fingerprint-drift.sh A B}
+t=$(mktemp -d); trap 'rm -rf -- "$t"' EXIT
+# "path<TAB>digest", keyed on path; awk keeps names with spaces whole.
+key() { awk '{ d = substr($0, 1, 64); p = substr($0, 67); print p "\t" d }' "$1" | LC_ALL=C sort -t "$(printf '\t')" -k1,1; }
+key "$a" > "$t/a"; key "$b" > "$t/b"
+LC_ALL=C join -t "$(printf '\t')" -a 1 -a 2 -e MISSING -o 0,1.2,2.2 "$t/a" "$t/b" \
+  | awk -F '\t' '$2 != $3 { print $1 }' > "$t/drift"
+# Keep a path only if no other drifting path lies beneath it.
+awk 'NR == FNR { all[$0] = 1; next }
+     { for (q in all) if (index(q, $0 "/") == 1) next; print }' "$t/drift" "$t/drift" | LC_ALL=C sort
diff --git a/scripts/ci/fs-fingerprint.sh b/scripts/ci/fs-fingerprint.sh
new file mode 100755
index 00000000..331eb059
--- /dev/null
+++ b/scripts/ci/fs-fingerprint.sh
@@ -0,0 +1,97 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# fs-fingerprint.sh DEPTH < image.tar
+#
+# Reads a filesystem tar stream (`podman export`) on stdin and prints one
+# line, "<sha256>  <path>", for every path at most DEPTH components deep.
+# A regular file's digest covers its content and permissions; a symlink's
+# or hard link's covers its target; a directory's covers every entry beneath
+# it (type, permissions, path, and content digest or link target).
+#
+# Comparing two builds path by path then names where they drift, not only
+# which layer. Nothing is extracted: content is hashed as it streams past.
+# Owners and timestamps are deliberately left out (`podman build
+# --timestamp` fixes the times; owners are not what reproducibility means).
+#
+# Names are untrusted (they come from an image). They are never put into a
+# shell command: names and link targets are read from tar's C-quoted
+# listing, which is lossless (spaces, tabs, quotes and newlines survive as
+# escapes), content digests are matched to entries by archive order, and
+# directory digests are computed over numbered group files.
+set -euo pipefail
+depth=${1:?usage: fs-fingerprint.sh DEPTH < image.tar}
+[[ $depth =~ ^[1-9][0-9]*$ ]] || { echo "fs-fingerprint: DEPTH must be a positive integer" >&2; exit 2; }
+for tool in tar sha256sum awk sort join xargs; do
+  command -v "$tool" >/dev/null || { echo "fs-fingerprint: $tool missing" >&2; exit 2; }
+done
+tar --version | head -n 1 | grep -q 'GNU tar' || { echo "fs-fingerprint: GNU tar required" >&2; exit 2; }
+
+work=$(mktemp -d)
+trap 'rm -rf -- "$work"' EXIT
+mkfifo "$work/stream"
+export LC_ALL=C
+
+# Single read of stdin, split two ways. The --to-command runs once per
+# regular file in archive order and prints only that file's digest: the
+# file name is not used, so it cannot be interpreted.
+tee "$work/stream" \
+  | tar -x --to-command='sha256sum | cut -c1-64' -f - > "$work/digests" &
+hasher=$!
+tar --quoting-style=c -tv --numeric-owner -f - < "$work/stream" > "$work/listing"
+wait "$hasher"
+
+# Manifest rows: "<path>\t<type>\t<perms>\t<digest-or-target>", where path
+# and target keep tar's C escapes (no raw tab or newline can occur), with a
+# leading "./" or "/" removed. Regular files take the next digest in order.
+awk -v digests="$work/digests" '
+  # The i-th C-quoted string ("...", with \" escapes) on the line.
+  function quoted(s, which,    i, c, n, start, out, inq) {
+    n = 0; inq = 0; out = ""
+    for (i = 1; i <= length(s); i++) {
+      c = substr(s, i, 1)
+      if (!inq) { if (c == "\"") { inq = 1; out = "" } continue }
+      if (c == "\\") { out = out c substr(s, i + 1, 1); i++; continue }
+      if (c == "\"") { inq = 0; if (++n == which) return out; continue }
+      out = out c
+    }
+    return ""
+  }
+  function clean(p) { sub(/^\.?\//, "", p); sub(/\/$/, "", p); return p }
+  {
+    t = substr($1, 1, 1); perm = substr($1, 2)
+    name = clean(quoted($0, 1))
+    if (t == "-" || t == "C") {
+      if ((getline d < digests) <= 0) { print "fs-fingerprint: fewer digests than files" > "/dev/stderr"; exit 3 }
+      if (name != "") printf "%s\tf\t%s\t%s\n", name, perm, d
+    }
+    else if (name == "") next
+    else if (t == "d") printf "%s\td\t%s\t-\n", name, perm
+    else if (t == "l") printf "%s\tl\t%s\t%s\n", name, perm, quoted($0, 2)
+    else if (t == "h") printf "%s\th\t%s\t%s\n", name, perm, clean(quoted($0, 2))
+    else printf "%s\t%s\t%s\t-\n", name, t, perm
+  }
+  END { if ((getline d < digests) > 0) { print "fs-fingerprint: more digests than files" > "/dev/stderr"; exit 3 } }
+' "$work/listing" | sort -t "$(printf '\t')" -k1,1 > "$work/manifest"
+
+# Every row is credited to each ancestor prefix up to DEPTH. awk writes
+# each prefix's rows to a numbered file (the number, not the name, is the
+# file name) and an index "number<TAB>prefix"; sha256sum then hashes the
+# numbered files, and join maps digests back to prefixes.
+mkdir "$work/g"
+awk -v depth="$depth" -v dir="$work/g" -F '\t' '
+  {
+    n = split($1, part, "/"); prefix = ""
+    for (k = 1; k <= n && k <= depth; k++) {
+      prefix = prefix (k == 1 ? "" : "/") part[k]
+      if (!(prefix in id)) { id[prefix] = ++count; printf "%d\t%s\n", count, prefix > (dir "/index") }
+      print $0 >> (dir "/" id[prefix])
+      # Keep the number of open files bounded on large images.
+      close(dir "/" id[prefix])
+    }
+  }' "$work/manifest"
+[[ -s "$work/g/index" ]] || exit 0
+(cd "$work/g" && find . -maxdepth 1 -type f ! -name index -printf '%f\0' \
+   | xargs -0 sha256sum | awk '{ print $2 "\t" $1 }' | sort -t "$(printf '\t')" -k1,1) > "$work/sums"
+sort -t "$(printf '\t')" -k1,1 "$work/g/index" \
+  | join -t "$(printf '\t')" -o 2.2,1.2 - "$work/sums" \
+  | awk -F '\t' '{ print $1 "  " $2 }' | sort -k2
diff --git a/scripts/ci/install-isabelle.sh b/scripts/ci/install-isabelle.sh
new file mode 100755
index 00000000..558a1c3e
--- /dev/null
+++ b/scripts/ci/install-isabelle.sh
@@ -0,0 +1,56 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# install-isabelle.sh — install the pinned Isabelle release into
+# /opt/isabelle and link /usr/local/bin/isabelle. Used by every workflow
+# that needs Isabelle (live-provers T2, verification-proofs-cron), so the
+# version, digest and mirrors live in one place.
+#
+# Why the mirror list: the upstream `dist/` path holds only the current
+# release, so a pinned release 404s once the next one ships (weekly
+# Isabelle/HOL, 2026-11-09). isabelle.in.tum.de has also redirected to an
+# http:// mirror, which `--proto-redir =https` refuses (T2 nightly). Each
+# release stays published under `website-<release>/dist/`. Every candidate
+# is fetched over https only, and the tarball must match the pinned
+# SHA-256 whichever host served it.
+#
+# Exit codes: 0 installed and `isabelle version` ran, 1 no mirror served the
+# pinned tarball, or the install failed.
+set -euo pipefail
+
+RELEASE=Isabelle2025-2
+SHA256=a20a507bc7c1270d8be96a9f3fbec06345387789d2dc2c4d3df6260d47bfb33c
+TARBALL="${RELEASE}_linux.tar.gz"
+MIRRORS=(
+  "https://isabelle.in.tum.de/website-${RELEASE}/dist/${TARBALL}"
+  "https://www.cl.cam.ac.uk/research/hvg/Isabelle/website-${RELEASE}/dist/${TARBALL}"
+  "https://isabelle.sketis.net/website-${RELEASE}/dist/${TARBALL}"
+  "https://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/${TARBALL}"
+  "https://isabelle.in.tum.de/dist/${TARBALL}"
+)
+
+dest="${RUNNER_TEMP:-/tmp}/${TARBALL}"
+fetched=""
+for url in "${MIRRORS[@]}"; do
+  echo "install-isabelle: trying $url"
+  rm -f "$dest"
+  if curl --proto '=https' --proto-redir '=https' -fL --connect-timeout 20 --max-time 420 \
+       --retry 2 --retry-delay 10 --retry-max-time 420 --retry-all-errors -o "$dest" "$url" \
+     && printf '%s  %s\n' "$SHA256" "$dest" | sha256sum --check --status; then
+    fetched="$url"
+    break
+  fi
+  echo "install-isabelle: $url did not serve the pinned tarball" >&2
+done
+if [ -z "$fetched" ]; then
+  echo "::error::install-isabelle: no mirror served ${TARBALL} with SHA-256 ${SHA256}" >&2
+  exit 1
+fi
+echo "install-isabelle: ${TARBALL} from $fetched (SHA-256 verified)"
+
+sudo mkdir -p /opt/isabelle
+sudo tar xzf "$dest" -C /opt/isabelle
+sudo ln -sf "/opt/isabelle/${RELEASE}/bin/isabelle" /usr/local/bin/isabelle
+rm -f "$dest"
+isabelle version
diff --git a/scripts/ci/test-fs-fingerprint.sh b/scripts/ci/test-fs-fingerprint.sh
new file mode 100755
index 00000000..6615833f
--- /dev/null
+++ b/scripts/ci/test-fs-fingerprint.sh
@@ -0,0 +1,74 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Self-test for scripts/ci/fs-fingerprint.sh: identical trees agree, and a
+# content, mode or link-target change is reported at the changed path and
+# its ancestors only. Names with spaces, "|" and "&" survive intact.
+set -euo pipefail
+here=$(cd "$(dirname "$0")" && pwd)
+t=$(mktemp -d); trap 'rm -rf -- "$t"' EXIT
+fp() { (cd "$1" && tar --sort=name -cf - .) | bash "$here/fs-fingerprint.sh" "$2"; }
+fail() { echo "FAIL: $*" >&2; exit 1; }
+
+mkdir -p "$t/a/opt/elan/toolchains/lean/lib" "$t/a/usr/bin"
+echo hi > "$t/a/usr/bin/x"
+echo lean > "$t/a/opt/elan/toolchains/lean/lib/a.olean"
+echo s > "$t/a/opt/elan/settings.toml"
+ln -s ../usr/bin/x "$t/a/opt/link"
+echo odd > "$t/a/opt/we|ird &name"
+chmod 0644 "$t/a/usr/bin/x"
+
+clone() { rm -rf "$t/b"; cp -a "$t/a" "$t/b"; }
+changed() { diff <(fp "$t/a" "$1") <(fp "$t/b" "$1") | sed -n 's/^> [0-9a-f]\{64\}  //p' | sort | tr '\n' ' '; }
+
+clone
+[[ -z $(changed 4) ]] || fail "identical trees differ"
+fp "$t/a" 2 | grep -qx '[0-9a-f]\{64\}  opt/we|ird &name' || fail "odd name lost"
+
+echo changed > "$t/b/opt/elan/toolchains/lean/lib/a.olean"
+[[ $(changed 3) == "opt opt/elan opt/elan/toolchains " ]] || fail "deep content change: $(changed 3)"
+[[ $(changed 6) == "opt opt/elan opt/elan/toolchains opt/elan/toolchains/lean opt/elan/toolchains/lean/lib opt/elan/toolchains/lean/lib/a.olean " ]] \
+  || fail "deep content change at depth 6: $(changed 6)"
+
+clone; chmod 0755 "$t/b/usr/bin/x"
+[[ $(changed 3) == "usr usr/bin usr/bin/x " ]] || fail "mode change: $(changed 3)"
+
+clone; ln -sfn ../usr/bin/y "$t/b/opt/link"
+[[ $(changed 2) == "opt opt/link " ]] || fail "link target change: $(changed 2)"
+
+# fs-fingerprint-drift.sh names the deepest differing paths, odd names whole.
+clone; echo changed > "$t/b/opt/elan/toolchains/lean/lib/a.olean"; echo x > "$t/b/opt/we|ird &name"
+rm "$t/b/usr/bin/x"
+fp "$t/a" 9 > "$t/fa"; fp "$t/b" 9 > "$t/fb"
+leaves=$(bash "$here/fs-fingerprint-drift.sh" "$t/fa" "$t/fb" | tr "\n" "|")
+[[ $leaves == "opt/elan/toolchains/lean/lib/a.olean|opt/we|ird &name|usr/bin/x|" ]] || fail "drift leaves: $leaves"
+[[ -z $(bash "$here/fs-fingerprint-drift.sh" "$t/fa" "$t/fa") ]] || fail "self-drift not empty"
+
+if echo | bash "$here/fs-fingerprint.sh" 0 2>/dev/null; then fail "depth 0 accepted"; fi
+# Untrusted names never reach a shell: a name that is a command substitution
+# stays data, and nothing runs.
+clone; touch "$t/b/opt/a\$(touch PWNED)" "$t/b/opt/a\`touch PWNED\`" "$t/b/opt/q\"uote's"
+# Run from a scratch directory, where an injected relative `touch` would land.
+mkdir -p "$t/cwd"
+(cd "$t/cwd" && fp "$t/b" 3) > "$t/fb" 2>/dev/null
+[[ ! -e "$t/cwd/PWNED" && ! -e "$t/b/PWNED" ]] || fail "a file name was executed"
+grep -qF "opt/q\\\"uote's" "$t/fb" || fail "quote in a name lost"
+grep -qF "opt/a\$(touch" "$t/fb" || fail "command-substitution name lost"
+
+# Hard links: the name and its target are parsed apart ("link to").
+clone; ln "$t/b/usr/bin/x" "$t/b/usr/bin/hard"
+fp "$t/b" 3 | grep -qx "[0-9a-f]\{64\}  usr/bin/hard" || fail "hard link name mis-parsed"
+
+# Whitespace inside a link target and a tab inside a name are lossless.
+clone; ln -sfn "target value" "$t/a/opt/sp"; ln -sfn "target  value" "$t/b/opt/sp"
+[[ $(changed 2) == *"opt/sp "* ]] || fail "double space in a link target not detected"
+clone; touch "$t/a/opt/tab$(printf '\t')a" "$t/b/opt/tab$(printf '\t')b"
+[[ $(fp "$t/a" 2 | grep -c 'opt/tab\\ta$') == 1 && $(changed 2) == *"opt/tab\\tb"* ]] \
+  || fail "tab names collided or were truncated: $(changed 2)"
+
+# Owners and timestamps are not part of the fingerprint.
+clone
+A=$( (cd "$t/a" && tar --sort=name --owner=0 --group=0 --mtime=@0 -cf - .) | bash "$here/fs-fingerprint.sh" 4)
+B=$( (cd "$t/b" && tar --sort=name --owner=4242 --group=4242 --mtime=@1700000000 -cf - .) | bash "$here/fs-fingerprint.sh" 4)
+[[ "$A" == "$B" ]] || fail "owner or mtime changed the fingerprint"
+
+echo "PASS: fs-fingerprint names exactly the changed paths (content, mode, link target, hard links); names stay data; owners and times are ignored"
diff --git a/scripts/ci/test-issue-regressions.sh b/scripts/ci/test-issue-regressions.sh
index b1433f7a..4c404e01 100644
--- a/scripts/ci/test-issue-regressions.sh
+++ b/scripts/ci/test-issue-regressions.sh
@@ -110,6 +110,13 @@ fi
 grep -q 'allow-fail units checked: 1$' "$tmp/allow-fail.log"
 grep -q 'units.yml:7: continue-on-error without' "$tmp/allow-fail.log"
 
+# An explicit empty --today is an error, not a fall-back to FAKE_DATE (an
+# earlier FAKE_DATE would otherwise accept an expired unit).
+rc=0
+FAKE_DATE=2020-01-01 bash scripts/ci/check-allow-fail-expiry.sh --today "" "$tmp/allow-fail" \
+  > /dev/null 2>&1 || rc=$?
+[ "$rc" -eq 2 ] || { echo "FAIL: empty --today gave exit $rc, expected 2" >&2; exit 1; }
+
 # Managed workflows start with an actions-lock comment, not the SPDX header.
 # Inspect the comment preamble rather than assuming the licence is line one.
 # Top-level `permissions` is read with yq (YAML-POLICY Y-1): in KYAML it is