diff --git a/.github/workflows/contract-gate.yml b/.github/workflows/contract-gate.yml
index 41157d6..7d27b61 100644
--- a/.github/workflows/contract-gate.yml
+++ b/.github/workflows/contract-gate.yml
@@ -56,7 +56,11 @@ jobs:
   # cannot).
   kernel-proofs:
     name: Grade kernel proofs (Idris2 0.8.0 + Agda)
-    runs-on: ubuntu-latest
+    # Pinned: the job installs Agda from apt, so the image decides the Agda
+    # version, and the reject checks need 2.6.3 (tools/check-kernel-proofs.sh
+    # refuses any other). ubuntu-latest moved to 26.04 (Agda 2.8.0) on
+    # 2026-10-19.
+    runs-on: ubuntu-24.04
     timeout-minutes: 40
     env:
       IDRIS2_COMMIT: 15a3e4e70843f7a34100f6470c04b791330788df  # v0.8.0
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index 834cca1..dbff89f 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -9,6 +9,18 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 
 === [Unreleased]
 
+==== Kernel proofs pinned to Agda 2.6.3 (2026-10-26)
+
+* `ubuntu-latest` moved to Ubuntu 26.04 on 2026-10-19, so the Contract
+  Gate's kernel-proofs job, which installs Agda from apt, got Agda 2.8.0.
+  2.8.0 prints error locations as `file:11.38` where 2.6.3 printed
+  `file:11,38`, and occupancy-types' own reject check accepts only the old
+  form, so it reported `CostIsOccupancy` as an unexpected failure although
+  Agda refused it correctly.
+* The job now runs on `ubuntu-24.04`, whose `agda-bin` is 2.6.3, and
+  `tools/check-kernel-proofs.sh` refuses any other Agda (as it already
+  refuses any Idris2 but 0.8.0), unless `ALLOW_ANY_AGDA=1` is set.
+
 ==== occupancy-types pin `6013483` → `8f09c0b` (2026-10-14)
 
 * `scripts/fetch-siblings.sh` pins occupancy-types at `8f09c0b`, the merge of
diff --git a/tools/check-kernel-proofs.sh b/tools/check-kernel-proofs.sh
index 8f5757e..043c403 100755
--- a/tools/check-kernel-proofs.sh
+++ b/tools/check-kernel-proofs.sh
@@ -48,6 +48,13 @@ case "$iv" in
   *"version 0.8.0"*) ;;
   *) [ -n "${ALLOW_ANY_IDRIS2:-}" ] || die "Idris2 0.8.0 required (src/abi targets 0.8.0; EXPECT messages are 0.8.0's). Set ALLOW_ANY_IDRIS2=1 to try another." ;;
 esac
+# The rejection checks match prover messages and locations, and both change
+# between Agda releases: 2.8.0 prints `file:11.38` where 2.6.3 printed
+# `file:11,38`, which occupancy-types' own reject check does not accept.
+case "$av" in
+  "Agda version 2.6.3") ;;  # the whole line: 2.6.3.1 is another release
+  *) [[ -n "${ALLOW_ANY_AGDA:-}" ]] || die "Agda 2.6.3 required (the pinned siblings' reject checks expect 2.6.3's messages). Set ALLOW_ANY_AGDA=1 to try another." ;;
+esac
 [ -d "$RA/src/ResourceAlgebra" ] || die "resource-algebra not fetched — run scripts/fetch-siblings.sh"
 echo "resource-algebra at $(git -C "$RA" rev-parse HEAD)"
 rm -rf "$OUT"; mkdir -p "$OUT"