diff --git a/.github/workflows/agda-proofs.yml b/.github/workflows/agda-proofs.yml
index 2f53eef..4399a3c 100644
--- a/.github/workflows/agda-proofs.yml
+++ b/.github/workflows/agda-proofs.yml
@@ -1,7 +1,7 @@
 # SPDX-License-Identifier: MPL-2.0
 # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 name: Agda proofs
-# DESIGNED until its first green run. Pattern: choreographic-types /
+# First green run 2026-10-13, Agda 2.6.4.3 (PR #150). Pattern: choreographic-types /
 # residual-evidence-types (pinned Debian prover, sibling fetched by commit).
 # Checks verification/proofs/agda/Reversibility.agda under the kernel flags
 # and refuses the fixtures under tests/reject-agda. Local run: just test-agda.
@@ -15,6 +15,7 @@ jobs:
   proofs:
     name: Reversibility as a grade (Loss instance), expected rejections
     runs-on: ubuntu-latest
+    timeout-minutes: 15
     # trixie-slim, resolved 2026-10-13; re-pin deliberately, like the prover below.
     container: debian:trixie-slim@sha256:a29215f6a35e51e22adffa17f89e9d2ef06214e64a2bad10d765c46aea49f11f
     steps:
diff --git a/ffi/zig/include/januskey.h b/ffi/zig/include/januskey.h
index 18c595f..e548ac6 100644
--- a/ffi/zig/include/januskey.h
+++ b/ffi/zig/include/januskey.h
@@ -2,7 +2,7 @@
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 /* SPDX-License-Identifier: MPL-2.0 */
 /* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) */
-/* JanusKey C FFI Header — hand-maintained; src/abi/JanusKey/ABI/Foreign.idr must mirror it (checked by the ABI package typecheck) */
+/* JanusKey C FFI Header — hand-maintained; src/abi/JanusKey/ABI/Foreign.idr mirrors it: symbols, status codes, enums and sizes are compared by scripts/check-abi-layout.sh */
 
 #ifndef JANUSKEY_H
 #define JANUSKEY_H
diff --git a/scripts/check-abi-tree.sh b/scripts/check-abi-tree.sh
index 923e761..76b3f16 100755
--- a/scripts/check-abi-tree.sh
+++ b/scripts/check-abi-tree.sh
@@ -10,7 +10,7 @@ fail=0
 say() { echo "[check-abi-tree] $*"; }
 
 # 1. The symlink farm (PR #140, src/idris-abi/) is retired.
-if [ -e src/idris-abi ]; then say "FAIL: src/idris-abi exists (retired symlink farm)"; fail=1; fi
+if [ -e src/idris-abi ] || [ -L src/idris-abi ]; then say "FAIL: src/idris-abi exists (retired symlink farm)"; fail=1; fi
 
 # 2. Exactly one package file, and it is the one the gates name.
 n=$(find src/abi -name '*.ipkg' | wc -l)