@@ -103,7 +103,7 @@ Results were consistent, but they do not prove CI is green.
 
 | typed-wasm repo (`/home/user/typed-wasm`)
 | `cargo test` passes 197 (default features) or 209 (all features). Clippy is clean. All 6 examples build and verify. `tw build` silently stubs bodies it cannot lower (`twice(5)=0`, `parser.rs` ~L895) and the result is VERIFIED. No L5 index guard is emitted: `get_player_hp(0,150)` returns 0. Malformed `session` blocks are accepted. No capabilities carrier is emitted. `tests/e2e.sh` reports 47 passed with 8 skipped (idris2, zig, parser), which is a silent green. Codegen output does not export memory, so multi-module sharing is unexercised.
-| L2, L13-imports and L15 sit behind `unstable-*` features, so the default `tw-verify` build skips them. An unknown carrier version returns `Ok(vec![])` (`verify.rs:880,967`). An unknown ownership byte decodes to Unrestricted. The 33 Idris2 modules fail under Idris2 0.7.0 at one base-library API change (`Region.idr:179`); with that token adapted in a scratch copy all 33 build, the 13 reject fixtures fail as expected, and 269 table rows check. The pinned 0.8.0 build was not run. `verifierIsSound` is vacuous as a claim about the Rust verifier, because each `VerifierAccepts` constructor already holds the spec witness. `MkAttestation` is public, so attestations can be forged. `Proofs.idr` attests L11 and L12 as proven while `LEVEL-STATUS` calls them draft. The "ECHIDNA 10^5" and "88/88 parser tests" claims cannot be reproduced: `Parser.mjs` is absent and `src/parser/*.affine` does not parse.
+| L2, L13-imports and L15 sit behind `unstable-*` features, so the default `tw-verify` build skips them. An unknown carrier version returns `Ok(vec![])` (`verify.rs:880,967`). An unknown ownership byte decodes to Unrestricted. The 33 Idris2 modules fail under Idris2 0.7.0 at one base-library API change (`Region.idr:179`); with that token adapted in a scratch copy all 33 build, the 13 reject fixtures fail as expected, and 269 table rows check. Under the pinned Idris2 0.8.0 (`15a3e4e`, built from source 2026-11-09) the unmodified tree passes `tools/check-kernel-proofs.sh` in full: 33 modules with no `Error:` line, no `believe_me`/`assert_total`/`assert_smaller`/`idris_crash`, 13 rejections for the expected reason, the explorer reproducing all 197 rows of `ops.tsv`, 269 equalities accepted by both Agda and Idris2, and 4 wrong rows refused by both. The `Region.idr:179` failure is a 0.7.0 incompatibility only. `verifierIsSound` is vacuous as a claim about the Rust verifier, because each `VerifierAccepts` constructor already holds the spec witness. `MkAttestation` is public, so attestations can be forged. `Proofs.idr` attests L11 and L12 as proven while `LEVEL-STATUS` calls them draft. The "ECHIDNA 10^5" and "88/88 parser tests" claims cannot be reproduced: `Parser.mjs` is absent and `src/parser/*.affine` does not parse.
 | No L8, L9, L14 or L16 carriers. No wasmtime gate adapter. No WasmCert tie-back.
 
 | Coq `formal/` (20 files)
@@ -153,12 +153,12 @@ Results were consistent, but they do not prove CI is green.
 
 | absolute-zero
 | The 4 active Agda modules type-check, including under the canonical flags with stdlib 1.7.3 (its CI) and 2.3 (what echo-types uses). The Z3 OND checks pass. The archived Coq tree is 17/17 closed. `src/whitespace` has 1 failing test.
-| The Idris ABI builds under Idris2 0.7.0 (the repo pins 0.8.0 through a pack image). It has five `believe_me`: `Layout.idr:270` and `Proofs/DivMod.idr:92,104,114,124`. All five statements are true and provable, so those rows are ASSUMED, not PROVEN. `HasSize` and `HasAlignment` carry no information, so the size and alignment claims are vacuous. `PROOF-STATUS` and `wiki/ABI.md` overclaim on both points. In the Agda CNO, the termination and thermodynamic parts are vacuous.
+| The Idris ABI builds under Idris2 0.7.0 and under the Idris2 0.8.0 release (4 modules, no `Error:` line). CI pins a digest of the `idris2-pack` image instead; its install path names Idris2 commit `6ca00e72…` on `main` (reported version 0.8.0), not the v0.8.0 tag, and that image was not run here. It has five `believe_me`: `Layout.idr:270` and `Proofs/DivMod.idr:92,104,114,124`. All five statements are true and provable, so those rows are ASSUMED, not PROVEN. `HasSize` and `HasAlignment` carry no information, so the size and alignment claims are vacuous. `PROOF-STATUS` and `wiki/ABI.md` overclaim on both points. In the Agda CNO, the termination and thermodynamic parts are vacuous.
 | —
 
 | januskey
 | 135 tests pass. The Agda kernel and 4 reject fixtures pass against resource-algebra `cf9235c`.
-| The Idris ABI type-checks under Idris2 0.7.0 (4 modules) and its 3 reject fixtures fail as expected. `seqCNO` and `tamperBreaksLink` hold for the Idris model only, which the repo states honestly. The Zig C ABI is a stub (9 `TODO(#155)` sites). T-8 is non-atomic.
+| The Idris ABI type-checks under Idris2 0.7.0 and the 0.8.0 release (4 modules, no `Error:` line), and `scripts/check-idris-reject.sh` refuses its 3 reject fixtures for the expected reason under both. A planted well-typed fixture makes that script fail, so it fails closed. CI runs the same `idris2-pack` image digest as absolute-zero (Idris2 `main` at `6ca00e72…`, not the v0.8.0 tag), which was not run here. `seqCNO` and `tamperBreaksLink` hold for the Idris model only, which the repo states honestly. The Zig C ABI is a stub (9 `TODO(#155)` sites). T-8 is non-atomic.
 | No AffineScript seam today.
 
 | stdlib and aLib
@@ -856,9 +856,9 @@ Ratings run from 1 (poor) to 5 (strong). Column (a) is elegance plus correctness
 * Scope: all repos, read-only.
 * Isolation: one container image snapshot, recorded so later workflows can reuse it.
 * Gates: the M0 commands; `cd $TW && cargo test --workspace --all-features`; Coq gate `just -f $AS/formal/justfile check` plus a generated `Print Assumptions` over every assertion; every Agda theory entrypoint under exactly `agda --safe --without-K --cubical-compatible`. Record each entrypoint's mode: a file-pragma `--cubical` still passes that command line, so a cubical module counts only under a separately reviewed proof profile, and that obligation stays open until the review is recorded.
-* Idris2 0.7.0 builds from source in an agent sandbox (verified 2026-11-09, about 15 minutes): `apt-get install -y chezscheme`, `git clone --depth 1 --branch v0.7.0 https://github.com/idris-lang/Idris2`, then `cd Idris2 && make bootstrap SCHEME=chezscheme && make install PREFIX=/opt/idris2`. Put `/opt/idris2/bin` on `PATH` for every later step and agent (`export PATH=/opt/idris2/bin:$PATH`), so direct checks and `tools/check-proofs.sh` find it. Record this as a PROOF-POLICY §6 deviation until the Guix manifest or container provides it. Idris2 0.8.0, which typed-wasm pins, has not been built in a sandbox.
+* Idris2 0.7.0 builds from source in an agent sandbox (verified 2026-11-09, about 15 minutes): `apt-get install -y chezscheme`, `git clone --depth 1 --branch v0.7.0 https://github.com/idris-lang/Idris2`, then `cd Idris2 && make bootstrap SCHEME=chezscheme PREFIX=/opt/idris2 && make install PREFIX=/opt/idris2`. Pass `PREFIX` to `make bootstrap` as well as to `make install`: the prefix is compiled into the binary, and without it the libraries land in `$HOME/.idris2` while the Chez support files land under the prefix. Such an install type-checks but cannot run `--exec` or compiled programs, and still exits 0 (reproduced 2026-11-09). Put `/opt/idris2/bin` on `PATH` for every later step and agent (`export PATH=/opt/idris2/bin:$PATH`), so direct checks and `tools/check-proofs.sh` find it. Record this as a PROOF-POLICY §6 deviation until the Guix manifest or container provides it. Idris2 0.8.0, which typed-wasm pins, builds the same way from commit `15a3e4e70843f7a34100f6470c04b791330788df` (verified 2026-11-09, about 25 minutes), also as a §6 deviation; with `PREFIX` given to both steps, typed-wasm's `tools/check-kernel-proofs.sh` passes with no other environment set.
 * Lean: install the pinned toolchain from `releases.lean-lang.org` (`curl -sSLO https://releases.lean-lang.org/lean4/v<ver>/lean-<ver>-linux.tar.zst`, extract with `tar --zstd`), and record its SHA-256 as a PROOF-POLICY §6 deviation. The owner approved this on 2026-11-09. GitHub release downloads stay blocked, so elan is not the route.
-* Treat an Idris2 `--check` exit code of 0 as a pass only when its output also contains no `Error:` line.
+* Treat an Idris2 exit code of 0 as a pass only when its output also contains no `Error:`, `INTERNAL ERROR` or `Exception` line. This holds for `--check` with a missing import and for `--exec` and compiled programs when the Chez support files are missing (both reproduced 2026-11-09). A gate that runs a compiled program must compare its output, not only its exit code.
 * Stop if: a pinned prover cannot be provisioned. Record the leg as unavailable and continue with the others.
 * Output: a versioned toolchain manifest, kept out of the repo root.
 
@@ -1007,7 +1007,8 @@ wasmtime run --invoke get_player_hp examples/01-single-module.wasm 0 150
 * [ ] januskey: T-1..T-3 are engineering statements proved in Agda with no §4 exception recorded.
 * [ ] Estate-wide: Idris2 0.7.0 `--check` exits 0 when an import is missing. Every Idris2 gate in the estate that trusts only the exit code can pass falsely. This belongs in `standards` (a gate rule) and in each repo's check script.
 * [ ] absolute-zero: discharge or name the five `believe_me` lemmas as axioms, give `HasSize` and `HasAlignment` real content, and correct `PROOF-STATUS` and `wiki/ABI.md`.
-* [ ] typed-wasm: make `MkAttestation` private, reconcile `Proofs.idr` with `LEVEL-STATUS` on L11 and L12, refresh the stale `PROOF-NEEDS` module counts, and fix the e2e Idris job's 404 tarball URL. Confirm the `Region.idr` build under the pinned Idris2 0.8.0.
+* [ ] typed-wasm: make `MkAttestation` private, reconcile `Proofs.idr` with `LEVEL-STATUS` on L11 and L12, refresh the stale `PROOF-NEEDS` module counts, and fix the e2e Idris job's 404 tarball URL. (The `Region.idr` build under the pinned Idris2 0.8.0 is confirmed: the full kernel-proof gate passes, 2026-11-09.)
+* [ ] Estate: the Idris2 repos check against two different compilers. typed-wasm pins the v0.8.0 tag (`15a3e4e`); januskey and absolute-zero pin an `idris2-pack` image whose Idris2 is a later `main` commit (`6ca00e72…`, also reporting 0.8.0); anytype pins 0.7.0. A pass under one does not carry to another. Pick one pinned compiler per proof tier and record it in each repo's deed.
 * [ ] Every repo above that installs a prover outside Guix or its container needs a PROOF-POLICY §6 deviation record. None has one (anytype's tarball has no digest check; typell's install is unpinned).
 * [ ] mathesis: the catalogue rows for this plan's repos were refreshed with a new merge mode for the census, and these repos were added as reconciliation targets (mathesis PR). The theorem-level claims registry is still unbuilt there.
 * [ ] Issue trackers: update #563, #513, #553, #555, #601 and #623. These are outward-facing; confirm before posting.