diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock
index ed2ab1b..6d393d8 100644
--- a/.github/workflows/actions.lock
+++ b/.github/workflows/actions.lock
@@ -24,7 +24,7 @@ workflows:
     '.github/workflows/labels.yml': []
     '.github/workflows/lock-sync-gate.yml': []
     '.github/workflows/main-estate-audit.yml':
-        - 'hyperpolymath/cicd-suite@354c425571c1f27b66dd141daeb0e90fa0c26dd9'
+        - 'hyperpolymath/proven-cicd-and-workflows@354c425571c1f27b66dd141daeb0e90fa0c26dd9'
     '.github/workflows/mirror.yml':
         - 'actions/checkout@v7.0.1'
         - 'dtolnay/rust-toolchain@master'
@@ -114,16 +114,6 @@ dependencies:
         commit: 'sha1-cdf488f595d80d6e07e03d4674febd5ab45fa938'
         owner_id: 9919
         repo_id: 259445878
-    'hyperpolymath/cicd-suite@354c425571c1f27b66dd141daeb0e90fa0c26dd9':
-        ref: '354c425571c1f27b66dd141daeb0e90fa0c26dd9'
-        commit: 'sha1-354c425571c1f27b66dd141daeb0e90fa0c26dd9'
-        owner_id: 6759885
-        repo_id: 1326697643
-        uses:
-            - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
-            - 'hyperpolymath/cicd-suite@35868f090e4e42b142374d156f2d49a22ad577fd'
-            - 'hyperpolymath/cicd-suite@88c55e28f37b8dfc5a435e86f548737997746cc9'
-            - 'hyperpolymath/cicd-suite@c519c4520afbfe48f16aceb0706d7cfb1d649994'
     'hyperpolymath/cicd-suite@35868f090e4e42b142374d156f2d49a22ad577fd':
         ref: '35868f090e4e42b142374d156f2d49a22ad577fd'
         commit: 'sha1-35868f090e4e42b142374d156f2d49a22ad577fd'
@@ -152,6 +142,16 @@ dependencies:
         commit: 'sha1-2155aa26a21758f2ba119f61bc7e0e1981c106fb'
         owner_id: 6759885
         repo_id: 1275650185
+    'hyperpolymath/proven-cicd-and-workflows@354c425571c1f27b66dd141daeb0e90fa0c26dd9':
+        ref: '354c425571c1f27b66dd141daeb0e90fa0c26dd9'
+        commit: 'sha1-354c425571c1f27b66dd141daeb0e90fa0c26dd9'
+        owner_id: 6759885
+        repo_id: 1326697643
+        uses:
+            - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1'
+            - 'hyperpolymath/cicd-suite@35868f090e4e42b142374d156f2d49a22ad577fd'
+            - 'hyperpolymath/cicd-suite@88c55e28f37b8dfc5a435e86f548737997746cc9'
+            - 'hyperpolymath/cicd-suite@c519c4520afbfe48f16aceb0706d7cfb1d649994'
     'hyperpolymath/smtp-notify-action@v0.5.0':
         ref: 'v0.5.0'
         commit: 'sha1-c1c9fa07992a02c1fd3d67a0dc1b08cccb852aef'
diff --git a/.github/workflows/main-estate-audit.yml b/.github/workflows/main-estate-audit.yml
index 262042b..aaf3a98 100644
--- a/.github/workflows/main-estate-audit.yml
+++ b/.github/workflows/main-estate-audit.yml
@@ -32,4 +32,4 @@ permissions:
 
 jobs:
   estate:
-    uses: hyperpolymath/cicd-suite/.github/workflows/main-estate-audit.yml@354c425571c1f27b66dd141daeb0e90fa0c26dd9 # cicd-suite main
+    uses: hyperpolymath/proven-cicd-and-workflows/.github/workflows/main-estate-audit.yml@354c425571c1f27b66dd141daeb0e90fa0c26dd9 # proven-cicd-and-workflows (formerly cicd-suite)
diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
index 202f37e..3ef14d9 100644
--- a/CHANGELOG.adoc
+++ b/CHANGELOG.adoc
@@ -33,6 +33,18 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning].
 * `tools/environments/` — `environments.kyaml` (environment classes with a
   `measured` block), `probe-reachability.sh` and `hosts.txt` (experiment
   X1: reachability probe, HEAD by default, one-byte GET with `--get`).
+* `scripts/proof-check.sh`, called by every `proof-check-*` recipe, and
+  `tests/proof_check_test.sh`. Agda runs with PROOF-POLICY §2.1's
+  `--safe --without-K --cubical-compatible`. A missing checker is reported
+  `UNAVAILABLE` and the run exits 3, never a pass. The escape-hatch scan
+  reads code only, so comments and strings no longer trip it. Checkers run
+  on a copy, so they write nothing into the tree.
+* `verification/proofs/agda/bofj-kitt-proofs.agda-lib`, so Agda can find
+  the standard library through its registered libraries. `AGDA_STDLIB`
+  overrides this with an explicit path.
+* A `verus` entry in `tools/proof-toolchain/toolchain.kyaml`. The owner
+  ruling of 2026-11-07 made Verus a default Rust verifier beside Creusot
+  (PROOF-POLICY §1.2).
 
 ==== Fixed
 
@@ -59,6 +71,47 @@ addressed:
 * `Justfile` `container-init` renders the `VERSION` placeholder; the dogfood gate's
   summary counts the K9 files the hook validated, not every `*.k9` path.
 
+Proof artefacts brought in line with PROOF-POLICY (metadatastician/standards
+at `9bdf864`):
+
+* `just proof-check-all` could never pass. Its escape-hatch scan matched the
+  template's own "no postulate" and "NO Admitted" comments in all 8 proof
+  files. No CI job ran it.
+* The Agda recipe ran `agda --safe` without the §2.1 flags, and every recipe
+  exited 0 when its prover was missing.
+* `docs/status/PROOF-STATUS.adoc` now uses the §5 vocabulary with no
+  percentage. It records the 2026-11-09 session results (Agda 2.6.3 and
+  Coq 8.18 check their template files, ACL2 8.5 and HOL Light pass their
+  smoke fixtures, and the rest are not run). It also lists the obligations
+  the proposals name for other repositories.
+* `docs/status/PROOF-NEEDS.adoc` withdraws the template's ABI and typing
+  obligations, since this repository has no ABI, FFI or typed API. TP-2 had
+  put API typing in Lean, but §1 puts it in Idris2. The prover guide
+  recommended Lean for its Mathlib, which §2 forbids; it now summarises §1.
+* `tools/proof-toolchain/DESIGN.adoc` states the §6 deviation records the
+  installer must write for every entry installed other than through Guix or
+  the container.
+* The cartridge proposal now keeps the §5 status, the §2.2 correspondence
+  state and the §8 grade as three separate fields. The cartridges never
+  write a grade: Mathesis derives grades from their receipts. An Agda
+  receipt also carries its library pin and import cone.
+* Review of the new escape-hatch scan found three cases it missed or
+  misreported, all fixed with regression tests:
+  ** a Lean character literal such as `'"'` opened a phantom string that
+     hid a later `sorry`;
+  ** an Agda identifier containing `--` was read as a comment that hid a
+     later `postulate`;
+  ** `admit` was flagged in Agda, where it is an ordinary name. Patterns are
+     now chosen per language.
+* `scripts/proof-check.sh` also makes a relative `AGDA_STDLIB` absolute and
+  copies a linked proof directory as its contents.
+* `toolchain.kyaml` gives Verus's own Z3 a `verus-z3` entry. The deviation
+  records are written by the bundle build that owns the lock, and the
+  exemption from them follows the install route rather than the tool.
+* `.github/workflows/main-estate-audit.yml` calls the audit under cicd-suite's
+  new name, `hyperpolymath/proven-cicd-and-workflows`. Since the rename on
+  2026-11-09 the old name failed at startup with zero jobs.
+
 ==== Changed
 
 * `build/setup.sh` — when no system package provides `just`, setup runs
diff --git a/build/just/proofs.just b/build/just/proofs.just
index b124d7a..05376b7 100644
--- a/build/just/proofs.just
+++ b/build/just/proofs.just
@@ -4,151 +4,40 @@
 # FORMAL VERIFICATION (PROOFS)
 #
 # Imported by ../../Justfile via `import? "build/just/proofs.just"`.
-# Recipes here check formal proofs across Idris2, Lean4, Agda, and Coq, plus
-# scan for dangerous/unsafe constructs and report status. Run via
-# `just proof-check-all` for the full sweep.
+# The recipes call scripts/proof-check.sh, which follows the estate
+# PROOF-POLICY (metadatastician/standards, 3-practice/PROOF-POLICY.adoc):
+# Agda runs with the canonical `--safe --without-K --cubical-compatible`
+# invocation (§2.1), and a missing checker is reported UNAVAILABLE and fails
+# the run instead of passing (exit 3). Set AGDA_STDLIB to the standard
+# library's source directory if it is not a registered Agda library.
+#
+# The proof files here are RSR template material, not obligations of this
+# repository; docs/status/PROOF-STATUS.adoc records their status.
 
-# Check all formal proofs (Idris2 + Lean4 + Agda + Coq)
-proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-check-coq proof-scan-dangerous
-    @echo "=== All proof checks complete ==="
+# Check every proof file and scan for escape hatches
+proof-check-all:
+    scripts/proof-check.sh all
 
-# Check Idris2 proofs (ABI, types, dependent type proofs)
+# Check Idris2 proofs
 proof-check-idris2:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Idris2 proofs ==="
-    if ! command -v idris2 &>/dev/null; then
-        echo "SKIP: idris2 not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if idris2 --check "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Idris2 proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Idris2 proofs verified"
+    scripts/proof-check.sh idris2
 
-# Check Lean4 proofs
+# Check Lean 4 proofs
 proof-check-lean4:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Lean4 proofs ==="
-    if ! command -v lean &>/dev/null; then
-        echo "SKIP: lean not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if lean "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Lean4 proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Lean4 proofs verified"
+    scripts/proof-check.sh lean4
 
-# Check Agda proofs
+# Check Agda proofs (PROOF-POLICY §2.1 invocation)
 proof-check-agda:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Agda proofs ==="
-    if ! command -v agda &>/dev/null; then
-        echo "SKIP: agda not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/agda -name '*.agda' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if agda --safe "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Agda proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Agda proofs verified"
+    scripts/proof-check.sh agda
 
-# Check Coq proofs
+# Check Coq (Rocq) proofs
 proof-check-coq:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Checking Coq proofs ==="
-    if ! command -v coqc &>/dev/null; then
-        echo "SKIP: coqc not installed"
-        exit 0
-    fi
-    ERRORS=0
-    for f in $(find verification/proofs/coq -name '*.v' 2>/dev/null); do
-        echo -n "  Checking $f ... "
-        if coqc "$f" 2>/dev/null; then
-            echo "OK"
-        else
-            echo "FAIL"
-            ERRORS=$((ERRORS + 1))
-        fi
-    done
-    if [ "$ERRORS" -gt 0 ]; then
-        echo "FAIL: $ERRORS Coq proof(s) failed"
-        exit 1
-    fi
-    echo "PASS: All Coq proofs verified"
+    scripts/proof-check.sh coq
 
-# Scan for dangerous patterns in proof files (believe_me, sorry, Admitted, etc.)
+# Scan proof code (comments and strings ignored) for escape hatches
 proof-scan-dangerous:
-    #!/usr/bin/env bash
-    set -euo pipefail
-    echo "=== Scanning for dangerous patterns in proofs ==="
-    DANGEROUS=0
-    PATTERNS="believe_me|assert_total|postulate|sorry|Admitted|unsafeCoerce|Obj\.magic"
-    for f in $(find verification/proofs -name '*.idr' -o -name '*.lean' -o -name '*.agda' -o -name '*.v' 2>/dev/null); do
-        MATCHES=$(grep -nE "$PATTERNS" "$f" 2>/dev/null || true)
-        if [ -n "$MATCHES" ]; then
-            echo "  DANGEROUS: $f"
-            echo "$MATCHES" | sed 's/^/    /'
-            DANGEROUS=$((DANGEROUS + 1))
-        fi
-    done
-    if [ "$DANGEROUS" -gt 0 ]; then
-        echo "FAIL: $DANGEROUS file(s) contain dangerous patterns"
-        exit 1
-    fi
-    echo "PASS: No dangerous patterns found in proofs"
+    scripts/proof-check.sh scan
 
-# Show proof status summary
+# Show the proof ledger summary
 proof-status:
-    #!/usr/bin/env bash
-    echo "=== Proof Status ==="
-    echo ""
-    echo "Idris2: $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null | wc -l) files"
-    echo "Lean4:  $(find verification/proofs/lean4 -name '*.lean' 2>/dev/null | wc -l) files"
-    echo "Agda:   $(find verification/proofs/agda -name '*.agda' 2>/dev/null | wc -l) files"
-    echo "Coq:    $(find verification/proofs/coq -name '*.v' 2>/dev/null | wc -l) files"
-    echo "TLA+:   $(find verification/proofs/tlaplus -name '*.tla' 2>/dev/null | wc -l) files"
-    echo ""
-    # PROOF-STATUS may live at root, docs/status/ (post-#20), .md or .adoc (post-#23)
-    for candidate in docs/status/PROOF-STATUS.adoc docs/status/PROOF-STATUS.md PROOF-STATUS.adoc PROOF-STATUS.md; do
-        if [ -f "$candidate" ]; then
-            grep -E "^\| \*\*Total\*\*|^\| \*Total\*" "$candidate" 2>/dev/null || echo "(No summary row in $candidate)"
-            exit 0
-        fi
-    done
-    echo "(No PROOF-STATUS file found at root or docs/status/)"
+    @sed -n '/^== Ledger/,/^== /p' docs/status/PROOF-STATUS.adoc | sed '$d'
diff --git a/docs/proposals/awesome-estate-maths-proving.adoc b/docs/proposals/awesome-estate-maths-proving.adoc
index 66fbbfb..466dff6 100644
--- a/docs/proposals/awesome-estate-maths-proving.adoc
+++ b/docs/proposals/awesome-estate-maths-proving.adoc
@@ -270,7 +270,8 @@ Reading the roster against the tools the lists above name shows what
 
 |*PROOF-POLICY names them* (highest priority: the estate's own mapping
 cannot be dispatched through its own prover platform)
-|Creusot, Kani, Aeneas (with Charon), Lambdapi as a checker (Dedukti has a
+|Creusot, Verus (a default Rust verifier since 2026-11-07), Kani, Aeneas (with
+Charon), Lambdapi as a checker (Dedukti has a
 variant, Lambdapi only an exchange format), agda2dedukti as a translator,
 Yices (in the kit manifest as a backend).
 
diff --git a/docs/proposals/boj-prover-solver-cartridges.adoc b/docs/proposals/boj-prover-solver-cartridges.adoc
index daaf53f..23d1754 100644
--- a/docs/proposals/boj-prover-solver-cartridges.adoc
+++ b/docs/proposals/boj-prover-solver-cartridges.adoc
@@ -113,12 +113,21 @@ json`; the five-level trust hierarchy and the axiom scan are echidna's.
 |`provers_portfolio`
 |Same input, two or more provers; returns each verdict and the combined
 trust level (level 5 only when two independent small-kernel systems agree
-with certificates, per echidna's `confidence.rs`).
+with certificates, per echidna's `confidence.rs`). echidna's trust level is
+not a Proof Witness Grade (PROOF-POLICY §8.6) and is never reported as one.
 
 |`provers_recheck`
 |The PROOF-POLICY §2 route: an Agda proof transported through Dedukti to
 Rocq and Lean, with `transported` or `re-proved` recorded per leg and the
 statement comparison named. Needs the kit's `transport` entries present.
+The Agda leg runs as `agda --safe --without-K --cubical-compatible` (§2.1).
+Each leg's record carries the §2.2 fields: the exact proposition,
+assumptions, source revision, checker and library versions by lock hash,
+invocation and observed result. It also carries two separate values: the
+leg's §5 status and its §2.2 correspondence state (`AGDA-PENDING`,
+`AGDA-VERIFIED`, `COQ-CHECKED`, `LEAN-CHECKED`, `BRIDGE-PENDING`,
+`RECONCILED`, `COUNTEREXAMPLE`, `QUARANTINED`). A transported leg stays
+`ASSUMED` until the statement comparison is recorded (§2).
 
 |`provers_exchange`
 |Translate between Dedukti, Lambdapi, TPTP, SMT-LIB, OpenTheory, SMTCoq
@@ -181,7 +190,9 @@ through one implementation.
 Input is a source tree with contracts; the answer is a proof ledger in
 the PROOF-POLICY §5 vocabulary (`PROVEN`, `PROVEN-WITH-AXIOMS`, `TESTED`,
 `ASSUMED`, `OPEN`) with a receipt. This is the cartridge for the tools that
-sit *on* code rather than on proof files: Creusot and Kani for Rust, SPARK
+sit *on* code rather than on proof files: Creusot (with Pearlite contracts)
+and Verus for Rust, the default pair since 2026-11-07 (PROOF-POLICY §1.2),
+with Kani as a standing exception; SPARK
 for Ada, Aeneas for Rust-to-model, Dafny, Why3 and Cameleer, F*, and the
 estate's own verifiers as they arrive: Quintessence (Elixir/OTP, three
 layers, already producing TrustLevel 4 certificates), Apodeixis.jl (Julia;
@@ -195,8 +206,11 @@ bactarin has no repository in the estate listing).
 
 |`verifiers_list`
 |The language-to-verifier mapping this host can serve, from PROOF-POLICY
-§1 and the capability record: Rust → Creusot (+ Kani, Aeneas), Ada → SPARK,
-Elixir → Quintessence, Julia → Apodeixis.jl, and the §4 exceptions.
+§1 and the capability record: Rust → Creusot and Verus (+ Kani, Aeneas),
+Ada → SPARK, Elixir → Quintessence, Julia → Apodeixis.jl, and the §4
+exceptions. Where Creusot and Verus prove the same property, the ledger
+records how the two statements correspond. It does not count them as
+independent results, because they share solver trust (§1.2, §4.1).
 
 |`verifiers_verify`
 |`{path, language?, tool?, obligations?}` → the ledger: one row per
@@ -346,14 +360,31 @@ are Idris2:
   host holds.
 * The ledger row. The §5 vocabulary is a closed sum type; a `TESTED` row
   carries bounds and a `PROVEN` row carries a certificate reference by
-  construction.
+  construction. A recheck row carries the §2.2 correspondence state as a
+  second closed type in its own field, so the two can never be written
+  into each other's place, as §2.2 requires.
+
+Status, correspondence state and Proof Witness Grade are three separate
+fields (PROOF-POLICY §2.2, §8). The cartridges write the first two and never
+the third. Mathesis derives a theorem's grade from the receipts and
+correspondence records these tools emit, and it never assigns one
+(Mathesis `docs/standards/AUTHORITY.adoc`). So every receipt carries what
+that derivation needs: the source commit, each checker's version and lock
+hash, the invocation and safe-mode flags, and the observed result. An Agda
+receipt also carries the library pin (name, version and lock hash of the
+standard library or other library it imports) and its import cone. The cone
+is the root module, the flags in force and the postulate count across
+every transitively imported module (PROOF-POLICY §1.1). Without them, a
+dependency cannot be counted as checked rather than assumed.
 
 One theory statement is worth an Agda file: echidna's five trust levels
 form a chain, and a portfolio's level is the meet of its members' levels
 except for the one case (two independent small-kernel systems, both with
 certificates) that lifts to level 5. Stating that as a lattice property and
 rechecking it in Rocq and Lean per §2 is small, and it is the property an
-agent relies on when it reads `trust_level: 5`.
+agent relies on when it reads `trust_level: 5`. It is theory about echidna,
+so it belongs in `hyperpolymath/echidna`; this repository's
+`docs/status/PROOF-STATUS.adoc` lists it as `OPEN` there.
 
 == Aspects
 
diff --git a/docs/proposals/environment-of-environments.adoc b/docs/proposals/environment-of-environments.adoc
index cdcc969..7554111 100644
--- a/docs/proposals/environment-of-environments.adoc
+++ b/docs/proposals/environment-of-environments.adoc
@@ -71,9 +71,10 @@ environment offers.
 
 |`build/just/proofs.just`
 |`proof-check-*` recipes
-|Each recipe probes a binary with `command -v`; a missing prover is a SKIP
-that reads like a pass. PROOF-POLICY §6 says a leg that cannot run must say
-so, not pass silently.
+|Each recipe probed a binary with `command -v`, and a missing prover was a
+SKIP that read like a pass. PROOF-POLICY §2.1 and §6 say a leg that cannot
+run must say so, not pass silently. Fixed 2026-11-09: the recipes call
+`scripts/proof-check.sh`, which reports `UNAVAILABLE` and exits 3.
 |===
 
 [[measured]]
@@ -319,7 +320,10 @@ raised and the unsupported target is named.
 |Give `proof-check-*` a planted missing prover and a planted broken proof.
 |The missing prover yields `UNAVAILABLE` in the record and a non-zero exit
 where PROOF-POLICY §6 requires it; the broken proof fails. Both directions
-verified, as LANGUAGE-POLICY §3 asks of any gate.
+verified, as LANGUAGE-POLICY §3 asks of any gate. Run 2026-11-09 for the
+script, before the record exists: `tests/proof_check_test.sh` with stub
+checkers, and Agda 2.6.3 and Coq 8.18 on a planted broken proof and a
+planted `Admitted`. The record half waits for E2.
 |===
 
 == The formal route
@@ -382,7 +386,8 @@ rather than lost:
   the record for "is Isabelle here".
 * `hyperpolymath/rsr-template-repo`: the `proof-check-*` recipes that `SKIP`
   on a missing prover are inherited by every repo; the fix belongs in the
-  template.
+  template. This repository's fix (`scripts/proof-check.sh`, 2026-11-09)
+  is the one to port.
 * The BoJ server's `ssg-mcp` cartridge needs a field for the record.
 
 == Decisions needed
diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc
index 1ff69d4..4f16379 100644
--- a/docs/status/PROOF-NEEDS.adoc
+++ b/docs/status/PROOF-NEEDS.adoc
@@ -1,121 +1,109 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Template: rsr-template-repo/docs/status/PROOF-NEEDS.adoc
-// Authoritative master list: ~/Desktop/PROOF-REQUIREMENTS-MASTER.adoc
-= Proof Requirements — BOFJ_KITT
+= Proof Requirements — bofj-kitt
 
-== Proof Tier
+Normative: the estate
+https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[PROOF-POLICY].
+It decides which prover carries which obligation. This file records what
+that means for this repository. Status lives in `PROOF-STATUS.adoc`.
 
-// Assign one: T1 (Critical), T2 (High), T3 (Standard), T4 (Light), T5 (Exempt)
-*Tier*: T3 — Standard
-
-== Proof Categories
+== Proof tier
 
-[cols="1,3,1", options="header"]
-|===
-| Code | Meaning | Applies?
-
-| *TP* | Typing Proofs (type soundness, type safety) | Yes
-| *INV* | Invariant Proofs (state machines, monotonicity, bounds) |
-| *SEC* | Security Proofs (crypto, injection freedom, access control) |
-| *CONC* | Concurrency Proofs (linearizability, deadlock freedom) |
-| *ALG* | Algorithm Proofs (termination, correctness, bounds) |
-| *ABI* | ABI/FFI Proofs (memory layout, pointer safety, platform compat) | Yes
-| *DOM* | Domain-Specific Proofs (bespoke to this project) |
-|===
+// Assign one: T1 (Critical), T2 (High), T3 (Standard), T4 (Light), T5 (Exempt)
+*Tier*: T5 — Exempt.
 
-== Mandatory Proofs (All RSR Repos)
+bofj-kitt is shell scripts, manifests and configuration. It has no ABI, no
+FFI, no typed API and no theory content, so PROOF-POLICY §1 maps nothing in
+it to a prover. Its scripts are covered by tests in `tests/`. Raise the tier
+if the repository gains code that §1 maps.
 
-These proofs come from the rsr-template-repo and MUST be present in every repo:
+== Template obligations, withdrawn
 
-=== ABI/FFI Boundary Proofs (Idris2)
+The RSR template lists these as mandatory for every repository. None of
+them has a subject here, so they are withdrawn rather than left as permanent
+"needed" rows. The template files themselves stay in `verification/proofs/`
+as template material.
 
-[cols="1,3,1,3", options="header"]
+[cols="1,3,3", options="header"]
 |===
-| # | Proof | Status | File
+|# |Template obligation |Why it does not apply
 
-| ABI-1 | Non-null pointer proofs (`So (ptr /= 0)`) | Needed | `verification/proofs/idris2/ABI/Pointers.idr`
-| ABI-2 | Memory layout correctness (`HasSize`, `HasAlignment`) | Needed | `verification/proofs/idris2/ABI/Layout.idr`
-| ABI-3 | Platform type size proofs (per platform) | Needed | `verification/proofs/idris2/ABI/Platform.idr`
-| ABI-4 | FFI function return type proofs | Needed | `verification/proofs/idris2/ABI/Foreign.idr`
-| ABI-5 | C ABI compliance (`CABICompliant`, `FieldsAligned`) | Needed | `verification/proofs/idris2/ABI/Compliance.idr`
-|===
+|ABI-1 to ABI-5
+|Pointer, layout, platform, FFI-return and C-ABI proofs (Idris2)
+|No ABI or FFI exists in this repository.
 
-=== Typing Proofs (Prover Varies)
+|TP-1
+|Core data type well-formedness (Idris2)
+|No typed data model exists in this repository.
 
-[cols="1,3,1,3", options="header"]
+|TP-2
+|Public API type safety; the template assigned it to Lean 4
+|No typed API exists here. Where it applies, PROOF-POLICY §1 assigns API
+properties to Idris2, not Lean.
 |===
-| # | Proof | Status | File
 
-| TP-1 | Core data type well-formedness | Needed | `verification/proofs/idris2/Types.idr`
-| TP-2 | Public API type safety (exported functions) | Needed | `verification/proofs/lean4/ApiTypes.lean`
-|===
+== Project-specific obligations
 
-== Project-Specific Proofs
+None. Obligations named by the proposals belong to the repositories that
+will hold the code; `PROOF-STATUS.adoc` lists them under "Obligations owned
+elsewhere".
 
-// Fill in proofs specific to this project. Copy from PROOF-REQUIREMENTS-MASTER.adoc
-// Delete this section for T4/T5 repos
+== Which prover (PROOF-POLICY §1)
 
-[cols="1,3,1,1,1,2", options="header"]
-|===
-| # | Proof Needed | Category | Prover | Priority | File(s)
+This section is a summary; PROOF-POLICY §1 is normative.
 
-| | | | | |
+[cols="2,2,3", options="header"]
 |===
+|Code or obligation |Verifier |Notes
 
-== Dangerous Patterns (BANNED)
+|Rust code
+|Creusot with Pearlite contracts, and Verus
+|Kani and Aeneas are standing exceptions (§4.1).
 
-The following MUST NOT appear anywhere in proof files:
+|Ada code
+|SPARK
+|
 
-[cols="2,2,3", options="header"]
-|===
-| Pattern | Language | Meaning
-
-| `believe_me` | Idris2 | Unsafe cast / trust-me
-| `assert_total` | Idris2 | Skip totality check
-| `postulate` | Idris2/Agda | Unproven axiom
-| `sorry` | Lean4 | Incomplete proof
-| `Admitted` | Coq | Incomplete proof
-| `unsafeCoerce` | Haskell | Unsafe type cast
-| `Obj.magic` | OCaml/AffineScript | Unsafe type cast
-| `unsafe` (unaudited) | Rust | Unsafe block without safety comment
+|APIs, ABIs and engineering properties
+|Idris2
+|Interface contracts, ABI layouts, wire formats, round trips.
+
+|Theory
+|Agda, rechecked in Rocq and Lean
+|Agda runs as `agda --safe --without-K --cubical-compatible` (§2.1). No
+Mathlib anywhere (§2).
 |===
 
-CI will reject any PR introducing these patterns (enforced by `panic-attack assail`).
+Any other tool (Isabelle/HOL, F*, TLA+, an SMT solver) needs a recorded §4
+exception. A finite model check, such as TLC, is `TESTED` with its bounds,
+not `PROVEN`.
+
+== Escape hatches
 
-== Prover Selection Guide
+`just proof-scan-dangerous` (`scripts/proof-check.sh scan`) fails on these
+words in proof code. Comments and string literals are ignored, so a comment
+that names a banned word does not trip it.
 
 [cols="2,2,3", options="header"]
 |===
-| Use Case | Recommended Prover | Why
-
-| ABI/FFI boundaries | *Idris2* | Dependent types model layouts precisely
-| Type system proofs | *Coq* or *Lean4* | Mature proof assistants for metatheory
-| Algebraic properties | *Lean4* | Good mathlib support
-| Inductive/coinductive | *Agda* | Native support for (co)induction
-| Distributed systems | *TLA+* | Model checking for protocols
-| Numerical properties | *Isabelle* | Strong real analysis library
+|Pattern |Language |Meaning
+
+|`believe_me` |Idris2 |Unchecked cast
+|`assert_total` |Idris2 |Skips the totality check
+|`postulate` |Agda, Idris2 |Unproven axiom
+|`TERMINATING`, `NON_TERMINATING`, `NO_TERMINATION_CHECK` |Agda pragmas |Skips the termination check
+|`sorry`, `admit` |Lean 4, Coq |Incomplete proof
+|`Admitted` |Coq |Incomplete proof
+|`unsafeCoerce` |Haskell |Unchecked cast
+|`Obj.magic` |OCaml |Unchecked cast
 |===
 
-== Proof File Locations
-
-----
-verification/proofs/
-├── idris2/          # Idris2 proofs (ABI, dependent types)
-│   ├── ABI/         # ABI-specific proofs
-│   └── *.idr        # Project-specific Idris2 proofs
-├── lean4/           # Lean4 proofs (algebra, lattices)
-│   └── *.lean
-├── agda/            # Agda proofs (induction, metatheory)
-│   └── *.agda
-├── coq/             # Coq proofs (type systems, compilation)
-│   └── *.v
-└── tlaplus/         # TLA+ specs (distributed protocols)
-    └── *.tla
-----
+How escape-hatch debt is budgeted and recorded is set by the standards
+repository's `docs/TRUSTED-BASE-REDUCTION-POLICY.adoc`, not here.
 
 == References
 
-* Master list: `~/Desktop/PROOF-REQUIREMENTS-MASTER.adoc`
-* Proof status tracking: `PROOF-STATUS.adoc` (this repo)
-* Proven library: `proven` repo (Idris2 verified foundations)
+* PROOF-POLICY: `metadatastician/standards`, `3-practice/PROOF-POLICY.adoc`
+* Estate proof needs: `metadatastician/standards`, `3-practice/PROOF-NEEDS.adoc`
+* Where estate proofs live: https://github.com/hyperpolymath/mathesis[mathesis]
 * Template: `rsr-template-repo/docs/status/PROOF-NEEDS.adoc`
diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc
index 6e60525..dee213b 100644
--- a/docs/status/PROOF-STATUS.adoc
+++ b/docs/status/PROOF-STATUS.adoc
@@ -1,100 +1,168 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Template: rsr-template-repo/docs/status/PROOF-STATUS.adoc
-// Tracks proof completion. Requirements defined in PROOF-NEEDS.adoc
-= Proof Status — BOFJ_KITT
+// Tracks proof status. Requirements are in PROOF-NEEDS.adoc.
+= Proof Status — bofj-kitt
+
+Normative: the estate
+https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[PROOF-POLICY],
+read at `9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5` (2026-11-08). Statuses
+use its closed §5 vocabulary: `PROVEN`, `PROVEN-WITH-AXIOMS`, `TESTED`,
+`ASSUMED`, `OPEN`. This file assigns no Proof Witness Grade (§8):
+Mathesis derives grades from receipts and never assigns them.
 
 == Summary
 
-[cols="2,1,1,1,1,1", options="header"]
-|===
-| Category | Total | Done | In Progress | Blocked | Remaining
-
-| ABI/FFI (ABI) | 5 | 0 | 0 | 0 | 5
-| Typing (TP) | 2 | 0 | 0 | 0 | 2
-| Invariant (INV) | 0 | 0 | 0 | 0 | 0
-| Security (SEC) | 0 | 0 | 0 | 0 | 0
-| Concurrency (CONC) | 0 | 0 | 0 | 0 | 0
-| Algorithm (ALG) | 0 | 0 | 0 | 0 | 0
-| Domain (DOM) | 0 | 0 | 0 | 0 | 0
-| *Total* | *7* | *0* | *0* | *0* | *7*
-|===
+bofj-kitt has *no first-party proof obligations*. It is shell scripts,
+manifests and configuration, with no ABI, no FFI, no typed API and no
+theory content, so the PROOF-POLICY §1 mapping assigns it nothing to
+prove. The behaviour of its scripts is covered by the tests in `tests/`,
+which are test evidence, not proofs.
 
-*Overall*: 0% proven
+Three kinds of proof-shaped files live here, and none of them is an
+obligation of this repository:
 
-== Proofs Done
+. RSR template proof files under `verification/proofs/`.
+. Prover-exercise fixtures under `tools/proof-toolchain/smoke/`.
+  PROOF-POLICY §3 puts corpora that exist to exercise provers outside the
+  policy.
+. Obligations the proposals name for code that will live in other
+  repositories.
 
-// Format:
-// | ID | Proof | Prover | File | Date | Verified By |
-// | ABI-1 | Non-null pointer proofs | Idris2 | verification/proofs/idris2/ABI/Pointers.idr | 2026-XX-XX | idris2 --check |
+== Ledger
 
-[cols="1,3,1,3,1,2", options="header"]
+[cols="1,4,1,1", options="header"]
 |===
-| ID | Proof | Prover | File | Date | Verified By
+|ID |Obligation |Prover (§1) |Status
 
-| — | No proofs completed yet | — | — | — | —
+4+|None. This repository has no first-party proof obligations.
 |===
 
-== Proofs In Progress
+== Template proof files
 
-[cols="1,3,1,2,1,2", options="header"]
-|===
-| ID | Proof | Prover | Assignee | Started | Blocker
+These files come from the RSR template and prove nothing about this
+repository. Mathesis's census sets them aside as template boilerplate. They
+are kept so the template's proof gates have something to check.
 
-| — | — | — | — | — | —
+The results below were taken in an agent session on 2026-11-09 with
+`scripts/proof-check.sh`. They are not CI receipts: no workflow runs these
+checks, and no source commit is pinned to them.
+
+[cols="2,2,3", options="header"]
 |===
+|File |Checker |Result (2026-11-09, session)
 
-== Proofs Blocked
+|`agda/Properties.agda`
+|Agda 2.6.3, standard library 1.7.3, `--safe --without-K --cubical-compatible`
+|Checked.
 
-[cols="1,3,2,3", options="header"]
-|===
-| ID | Proof | Blocked By | Notes
+|`coq/TypeSafety.v`
+|Coq 8.18.0
+|Checked. `Print Assumptions type_soundness`: closed under the global context.
+
+|`lean4/ApiTypes.lean`
+|Lean 4
+|Not run: no Lean toolchain available in the session.
 
-| — | — | — | —
+|`idris2/Types.idr`, `idris2/ABI/*.idr`
+|Idris2
+|Not run: no Idris2 toolchain available in the session.
+
+|`tlaplus/StateMachine.tla`
+|TLC
+|Not checked by any recipe. A TLC run would be `TESTED`, with its bounds (§4).
 |===
 
-== Proofs Remaining
+The escape-hatch scan (`just proof-scan-dangerous`) passes on all of them.
+It reads code only, so the template's own "no postulate" comments do not
+trip it.
+
+== Prover-exercise fixtures (PROOF-POLICY §3)
+
+`tools/proof-toolchain/smoke/` holds one trivial theorem per prover. Each
+one tests that a prover in the toolchain bundle runs and reports failure
+correctly. These files are test material, not obligations.
 
-[cols="1,3,1,1,1,1", options="header"]
+[cols="2,2,3", options="header"]
 |===
-| ID | Proof | Category | Prover | Priority | Est. Effort
-
-| ABI-1 | Non-null pointer proofs | ABI | Idris2 | P1 | 2h
-| ABI-2 | Memory layout correctness | ABI | Idris2 | P1 | 4h
-| ABI-3 | Platform type size proofs | ABI | Idris2 | P1 | 2h
-| ABI-4 | FFI function return type proofs | ABI | Idris2 | P1 | 2h
-| ABI-5 | C ABI compliance | ABI | Idris2 | P1 | 4h
-| TP-1 | Core data type well-formedness | TP | Idris2 | P1 | 4h
-| TP-2 | Public API type safety | TP | Lean4 | P2 | 4h
+|Fixture |Prover |Result (2026-11-09, session)
+
+|`acl2-smoke.lisp`
+|ACL2 8.5 (Ubuntu package)
+|Passes. A copy with a false theorem fails with exit 1.
+
+|`hol-light-refl.sh`
+|HOL Light 2023-10-21 (Ubuntu package, via a `hol_light` shim)
+|Passes. A copy expecting the wrong conclusion fails with
+"reflexivity smoke failed".
+
+|`hol4-smoke.sml`, `smoke.miz` with `mizar-smoke.sh`, `pvs_smoke.pvs` with `pvs-smoke.sh`
+|HOL4, Mizar, PVS
+|Not run: no package in the session. `tests/proof_smoke_wrappers_test.sh`
+covers the Mizar and PVS wrappers' pass and fail logic with stub provers.
 |===
 
-== Verification Commands
+== Obligations owned elsewhere
 
-[source,bash]
-----
-# Check all Idris2 proofs
-just proof-check-idris2
+The proposals name these obligations. Under §1 each one belongs to the
+repository that will hold the code, so they are listed here only so they
+are not lost.
 
-# Check all Lean4 proofs
-just proof-check-lean4
+[cols="3,1,2,1", options="header"]
+|===
+|Obligation |Prover (§1) |Home |Status
+
+|The cartridge `prover` argument type, derived from echidna's `ProverKind`
+|Idris2
+|`hyperpolymath/boj-server-cartridges`
+|`OPEN`
+
+|One `EnvCapability` record shared by `provers_list`, `solvers_list` and `verifiers_list`
+|Idris2
+|`hyperpolymath/boj-server-cartridges`
+|`OPEN`
+
+|The ledger row as a closed sum type: a `TESTED` row carries bounds, and a `PROVEN` row carries a checked certificate reference
+|Idris2
+|`hyperpolymath/boj-server-cartridges`
+|`OPEN`
+
+|echidna's trust levels form a chain, and a portfolio's level is the meet
+of its members' levels, except that two independent small-kernel systems
+that both have certificates lift the level to 5
+|Agda, rechecked in Rocq and Lean (§2)
+|`hyperpolymath/echidna`
+|`OPEN`
+|===
 
-# Check all Agda proofs
-just proof-check-agda
+== Toolchain deviations (PROOF-POLICY §6)
 
-# Check all Coq proofs
-just proof-check-coq
+None recorded. No workflow or recipe in this repository installs a proof
+toolchain yet. `tools/proof-toolchain/DESIGN.adoc` says which deviation
+records the installer must write when it lands.
 
-# Run all proof checks
-just proof-check-all
+== Verification commands
 
-# Scan for dangerous patterns
-panic-attack assail --proofs-only
+[source,bash]
+----
+just proof-check-all       # every leg, then the escape-hatch scan
+just proof-check-agda      # PROOF-POLICY §2.1 invocation
+just proof-check-coq
+just proof-check-lean4
+just proof-check-idris2
+just proof-scan-dangerous  # code only; comments and strings are ignored
 ----
 
+`scripts/proof-check.sh` exits 0 when every leg passes and 1 when a leg
+fails. It exits 3 when no leg failed but a checker was unavailable: a
+missing prover is reported, never passed. If the Agda standard library is
+not a registered Agda library, set `AGDA_STDLIB` to its source directory.
+
 == Changelog
 
 [cols="1,3,1", options="header"]
 |===
-| Date | Change | By
+|Date |Change |By
 
-| 2026-04-04 | Initial proof status tracking | Template
+|2026-04-04 |Initial proof status tracking |Template
+|2026-11-09 |Rewritten for PROOF-POLICY §5 and §8. Template obligations withdrawn (no ABI, FFI or typed API here). Session results and the fixture and owned-elsewhere tables added. |Claude Code
 |===
diff --git a/scripts/proof-check.sh b/scripts/proof-check.sh
new file mode 100755
index 0000000..9aa7307
--- /dev/null
+++ b/scripts/proof-check.sh
@@ -0,0 +1,220 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# proof-check.sh — check the proof files under verification/proofs/ and scan
+# them for escape hatches, following the estate PROOF-POLICY
+# (metadatastician/standards, 3-practice/PROOF-POLICY.adoc).
+#
+#   proof-check.sh [--proofs-dir DIR] LEG...
+#   LEG: agda | coq | lean4 | idris2 | scan | all
+#
+# Each leg reports one of PASS, FAIL or UNAVAILABLE. A missing checker is
+# UNAVAILABLE and makes the run fail: PROOF-POLICY §2.1 treats a missing tool
+# as an open obligation, so it is never reported as a pass or skipped silently.
+#
+# Agda runs with the canonical invocation of PROOF-POLICY §2.1:
+#   agda --safe --without-K --cubical-compatible <module.agda>
+# The standard library comes from AGDA_STDLIB (a directory holding its source)
+# when set; otherwise Agda resolves `depend: standard-library` in
+# verification/proofs/agda/*.agda-lib through its registered libraries.
+#
+# Checkers run on a temporary copy of the proofs directory, so their build
+# artefacts (.agdai, .vo, .glob, build/) never land in the working tree.
+#
+# Exit codes:
+#   0 — every requested leg passed
+#   1 — a leg failed (a proof did not check, or the scan found an escape hatch)
+#   2 — usage error
+#   3 — no leg failed, but at least one checker was unavailable
+
+set -euo pipefail
+
+# Print the invocation syntax to stderr and terminate the script with exit 2.
+usage() {
+    sed -n '/^#   proof-check.sh/,/^#   LEG:/p' "$0" | sed 's/^# \{0,3\}//' >&2
+    exit 2
+}
+
+proofs_dir="verification/proofs"
+legs=()
+while [ "$#" -gt 0 ]; do
+    case "$1" in
+        --proofs-dir) [ "$#" -ge 2 ] || usage; proofs_dir="$2"; shift 2 ;;
+        agda|coq|lean4|idris2|scan) legs+=("$1"); shift ;;
+        all) legs+=(agda coq lean4 idris2 scan); shift ;;
+        *) usage ;;
+    esac
+done
+[ "${#legs[@]}" -gt 0 ] || usage
+[ -d "$proofs_dir" ] || { echo "proof-check: no proofs directory at $proofs_dir" >&2; exit 2; }
+
+work="$(mktemp -d)"
+trap 'rm -rf "$work"' EXIT
+cp -RL "$proofs_dir/." "$work/"  # -L: a linked proof directory is copied, not left dangling
+
+failed=0
+unavailable=0
+# Print a leg result to stdout and set the global failed or unavailable flag
+# for FAIL or UNAVAILABLE respectively; PASS leaves both flags unchanged.
+report() {  # report <leg> <PASS|FAIL|UNAVAILABLE> <detail>
+    printf '%-7s %-11s %s\n' "$1" "$2" "$3"
+    case "$2" in
+        FAIL) failed=1 ;;
+        UNAVAILABLE) unavailable=1 ;;
+    esac
+}
+
+# run_files <leg> <tool> <subdir> <extension> <command-prefix...>
+# Check matching files recursively in the temporary copy of <subdir>, using
+# paths relative to that directory as the final command argument. <tool> is
+# checked on PATH; <extension> excludes the dot. Missing tools are reported as
+# UNAVAILABLE; missing directories, no matching files and checker failures are
+# reported as FAIL. Checker failures are collected so remaining files run;
+# these outcomes update global flags through report rather than returning an error.
+run_files() {
+    local leg="$1" tool="$2" sub="$3" ext="$4"; shift 4
+    if ! command -v "$tool" >/dev/null 2>&1; then
+        report "$leg" UNAVAILABLE "$tool is not on PATH; the check did not run"
+        return
+    fi
+    local dir="$work/$sub" n=0 bad=0 f
+    if [ ! -d "$dir" ]; then
+        report "$leg" FAIL "no $sub/ directory under $proofs_dir"
+        return
+    fi
+    echo "== $leg: $("$tool" --version 2>&1 | head -n 1)"
+    while IFS= read -r f; do
+        n=$((n + 1))
+        if (cd "$dir" && "$@" "${f#./}") >"$work/.log" 2>&1; then
+            echo "   ok   $sub/${f#./}"
+        else
+            bad=$((bad + 1))
+            echo "   FAIL $sub/${f#./}"
+            sed 's/^/        /' "$work/.log" | tail -n 20
+        fi
+    done < <(cd "$dir" && find . -name "*.$ext" -type f | LC_ALL=C sort)
+    if [ "$n" -eq 0 ]; then
+        report "$leg" FAIL "no .$ext files under $sub/"
+    elif [ "$bad" -gt 0 ]; then
+        report "$leg" FAIL "$bad of $n file(s) did not check"
+    else
+        report "$leg" PASS "$n file(s) checked"
+    fi
+}
+
+# Remove comments, keeping line numbers and Agda pragmas ({-# ... #-}), so the
+# scan sees only code. Nested block comments, string literals and character
+# literals ('"', '\'') are honoured. A quote after an identifier character is a
+# prime (`f'`), not a literal, and Coq has no character literals at all. In
+# Agda, `--` opens a comment only at the start of a token, since an identifier
+# such as `a--b` may contain it.
+strip_comments() {  # strip_comments <file>
+    local file="$1" line_tok open close doc='' agda=0 charlit=1
+    case "$file" in
+        *.idr) doc='|||' ;;  # Idris2 documentation comment, also a line comment
+        *.agda) agda=1 ;;
+    esac
+    case "$file" in
+        *.agda|*.idr) line_tok='--'; open='{-'; close='-}' ;;
+        *.lean)       line_tok='--'; open='/-'; close='-/' ;;
+        *.v)          line_tok='';   open='(*'; close='*)'; charlit=0 ;;
+        *) cat "$file"; return ;;
+    esac
+    LC_ALL=C awk -v lt="$line_tok" -v op="$open" -v cl="$close" -v doc="$doc" -v agda="$agda" -v charlit="$charlit" -v q="'" '
+        BEGIN { depth = 0 }
+        {
+            out = ""; i = 1; n = length($0); instr = 0
+            while (i <= n) {
+                two = substr($0, i, 2); c = substr($0, i, 1)
+                if (depth > 0) {
+                    if (two == op) { depth++; i += 2; continue }
+                    if (two == cl) { depth--; i += 2; continue }
+                    i++; continue
+                }
+                if (instr) {  # string contents are dropped: a word there is not code
+                    if (c == "\\") { i += 2; continue }
+                    if (c == "\"") { instr = 0; out = out c }
+                    i++; continue
+                }
+                pc = (i == 1) ? " " : substr($0, i - 1, 1)
+                # A quote after an identifier character (a byte >= 0x80 counts, for
+                # Unicode names) is a prime; otherwise it opens a character literal,
+                # dropped so a quote inside it is not taken for a string.
+                if (c == q && charlit && pc != q && pc !~ /[A-Za-z0-9_!?\200-\377]/) {
+                    if (substr($0, i + 1, 1) == "\\") {
+                        j = index(substr($0, i + 2), q)
+                        if (j > 0 && j <= 8) { i += j + 2; continue }
+                    } else if (substr($0, i + 2, 1) == q) { i += 3; continue }
+                }
+                if (c == "\"") { instr = 1; out = out c; i++; continue }
+                if (two == op && substr($0, i, 3) != "{-#") { depth = 1; i += 2; continue }
+                if (lt != "" && two == lt) {
+                    p = (i == 1) ? " " : substr($0, i - 1, 1)
+                    if (!agda || p ~ /[ \t(){};@".]/) break  # `.`: `...--` is a comment
+                }
+                if (doc != "" && substr($0, i, 3) == doc) break
+                out = out c; i++
+            }
+            print out
+        }' "$file"
+}
+
+# Escape hatches per language. A word that is an escape hatch in one language
+# can be an ordinary identifier in another (`admit` in Agda, say).
+hatch_pattern() {  # hatch_pattern <file>
+    case "$1" in
+        *.agda) echo 'postulate|TERMINATING|NON_TERMINATING|NO_TERMINATION_CHECK|unsafeCoerce' ;;
+        *.idr)  echo 'believe_me|assert_total|postulate|idris_crash' ;;
+        *.lean) echo 'sorry|admit' ;;
+        *.v)    echo 'Admitted|admit|Obj\.magic' ;;
+        *)      echo 'believe_me|assert_total|postulate|sorry|admit|Admitted|unsafeCoerce|Obj\.magic' ;;
+    esac
+}
+
+# Scan Agda, Idris2, Lean and Coq files in the temporary proof tree for each
+# language's escape-hatch patterns, ignoring comments and literals. Print
+# matches with source line numbers and report FAIL if any file has a match,
+# setting the global failed flag; an empty tree reports PASS.
+scan() {
+    local hits=0 f m
+    while IFS= read -r f; do
+        m="$(strip_comments "$work/$f" | grep -nwE "$(hatch_pattern "$f")" || true)"
+        if [ -n "$m" ]; then
+            hits=$((hits + 1))
+            echo "   escape hatch in ${f#./}:"
+            printf '%s\n' "$m" | sed 's/^/        /'
+        fi
+    done < <(cd "$work" && find . -type f \( -name '*.agda' -o -name '*.idr' -o -name '*.lean' -o -name '*.v' \) | LC_ALL=C sort)
+    if [ "$hits" -gt 0 ]; then
+        report scan FAIL "$hits file(s) contain an escape hatch in code"
+    else
+        report scan PASS "no escape hatch in code (comments ignored)"
+    fi
+}
+
+# Checkers run from inside the copy, so a relative library path is made
+# absolute against the caller's directory first.
+if [ -n "${AGDA_STDLIB:-}" ] && [ "${AGDA_STDLIB#/}" = "$AGDA_STDLIB" ]; then
+    AGDA_STDLIB="$PWD/$AGDA_STDLIB"
+fi
+
+for leg in "${legs[@]}"; do
+    case "$leg" in
+        agda)
+            if [ -n "${AGDA_STDLIB:-}" ]; then
+                run_files agda agda agda agda agda --safe --without-K --cubical-compatible \
+                    --no-libraries -i . -i "$AGDA_STDLIB"
+            else
+                run_files agda agda agda agda agda --safe --without-K --cubical-compatible
+            fi ;;
+        coq)    run_files coq coqc coq v coqc ;;
+        lean4)  run_files lean4 lean lean4 lean lean ;;
+        idris2) run_files idris2 idris2 idris2 idr idris2 --source-dir . --check ;;
+        scan)   scan ;;
+    esac
+done
+
+if [ "$failed" -ne 0 ]; then exit 1; fi
+if [ "$unavailable" -ne 0 ]; then exit 3; fi
+exit 0
diff --git a/tests/proof_check_test.sh b/tests/proof_check_test.sh
new file mode 100644
index 0000000..5f9506c
--- /dev/null
+++ b/tests/proof_check_test.sh
@@ -0,0 +1,132 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Test scripts/proof-check.sh against stub checkers and planted escape hatches.
+# It checks the invocations, the exit codes and the comment-aware scan; it does
+# not run Agda, Coq, Lean or Idris2 (run `just proof-check-all` for that).
+set -euo pipefail
+
+repo_root="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+check="$repo_root/scripts/proof-check.sh"
+work="$(mktemp -d)"
+trap 'rm -rf "$work"' EXIT
+
+fail() { echo "FAIL: $*" >&2; exit 1; }
+
+# Only the utilities the script needs, so provers installed on this machine
+# cannot answer for the stubs.
+mkdir -p "$work/sysbin" "$work/stubs"
+for tool in bash sed awk grep find sort cp mktemp rm head tail cat; do
+    ln -s "$(command -v "$tool")" "$work/sysbin/$tool"
+done
+
+# Each stub logs its arguments; STUB_FAIL names a checker that should fail.
+for tool in agda coqc lean idris2; do
+    cat > "$work/stubs/$tool" <<SH
+#!/bin/sh
+[ "\$1" = --version ] && { echo "$tool stub 0"; exit 0; }
+echo "\$*" >> "$work/$tool.args"
+[ "\${STUB_FAIL:-}" = "$tool" ] && exit 1
+: > built-artefact
+exit 0
+SH
+    chmod +x "$work/stubs/$tool"
+done
+
+run() {  # run <expected-exit> <PATH> <args...>; output goes to $work/out
+    local want="$1" path="$2"; shift 2
+    local got=0
+    PATH="$path" bash "$check" "$@" > "$work/out" 2>&1 || got=$?
+    [ "$got" -eq "$want" ] || { cat "$work/out" >&2; fail "proof-check $* exited $got, expected $want"; }
+}
+
+proofs="$repo_root/verification/proofs"
+before="$(cd "$proofs" && find . -type f -exec sha256sum {} + | LC_ALL=C sort)"  # names and contents
+
+# All checkers present and passing: canonical Agda flags, Idris2 source dir.
+run 0 "$work/stubs:$work/sysbin" --proofs-dir "$proofs" all
+grep -q -- '--safe --without-K --cubical-compatible Properties.agda' "$work/agda.args" ||
+    fail "agda not run with the PROOF-POLICY 2.1 invocation: $(cat "$work/agda.args")"
+grep -q -- '--source-dir . --check ABI/Compliance.idr' "$work/idris2.args" ||
+    fail "idris2 not run with a source directory: $(cat "$work/idris2.args")"
+grep -q '^scan    PASS' "$work/out" || fail "template comments tripped the scan"
+
+# AGDA_STDLIB switches to explicit include paths with library files ignored.
+: > "$work/agda.args"
+AGDA_STDLIB=/opt/stdlib run 0 "$work/stubs:$work/sysbin" --proofs-dir "$proofs" agda
+grep -q -- '--no-libraries -i . -i /opt/stdlib Properties.agda' "$work/agda.args" ||
+    fail "AGDA_STDLIB not passed as an include path: $(cat "$work/agda.args")"
+
+# A relative AGDA_STDLIB is resolved against the caller's directory, not the
+# copy the checker runs in.
+: > "$work/agda.args"
+(cd "$work" && AGDA_STDLIB=lib/stdlib run 0 "$work/stubs:$work/sysbin" --proofs-dir "$proofs" agda)
+grep -q -- "-i $work/lib/stdlib Properties.agda" "$work/agda.args" ||
+    fail "relative AGDA_STDLIB not made absolute: $(cat "$work/agda.args")"
+
+# A missing checker is UNAVAILABLE with exit 3, never a pass.
+rm "$work/stubs/lean"
+run 3 "$work/stubs:$work/sysbin" --proofs-dir "$proofs" all
+grep -q '^lean4   UNAVAILABLE' "$work/out" || fail "missing lean not reported UNAVAILABLE"
+
+# A failing checker fails the run, even with another one unavailable.
+STUB_FAIL=coqc run 1 "$work/stubs:$work/sysbin" --proofs-dir "$proofs" all
+grep -q '^coq     FAIL' "$work/out" || fail "failing coqc not reported"
+
+# The checkers ran on a copy: nothing was written into the tree.
+after="$(cd "$proofs" && find . -type f -exec sha256sum {} + | LC_ALL=C sort)"
+[ "$before" = "$after" ] || fail "a checker wrote into verification/proofs"
+
+# Scan: planted escape hatches in code fail; the same words in comments,
+# nested comments and strings do not.
+plant() {  # plant <relative-file> <content>; scan a tree holding only that file
+    rm -rf "$work/tree"; mkdir -p "$work/tree/$(dirname "$1")"
+    printf '%s\n' "$2" > "$work/tree/$1"
+}
+scan_expect() {  # scan_expect <exit> <relative-file> <content>
+    plant "$2" "$3"
+    run "$1" "$work/sysbin" --proofs-dir "$work/tree" scan
+}
+scan_expect 1 agda/A.agda 'postulate p : Set'
+scan_expect 1 agda/A.agda '{-# TERMINATING #-}'
+scan_expect 0 agda/A.agda '-- no postulate here'
+scan_expect 0 agda/A.agda '{- outer {- postulate -} still comment -} x = 1'
+scan_expect 1 agda/A.agda '{- comment -} postulate q : Set'
+scan_expect 1 idris2/B.idr 'f = believe_me x'
+scan_expect 0 idris2/B.idr '||| Docs mention assert_total
+-- and believe_me'
+scan_expect 1 coq/C.v 'Lemma l : True. Admitted.'
+scan_expect 0 coq/C.v '(* NO Admitted allowed (* nested *) *) Lemma l : True. exact I. Qed.'
+scan_expect 1 lean4/D.lean 'theorem t : True := by sorry'
+scan_expect 0 lean4/D.lean '/- sorry -/ def s := "sorry"'
+grep -q '^scan    PASS' "$work/out" || fail "comment and string not ignored"
+# A character literal holding a quote does not open a string that hides code.
+scan_expect 1 lean4/D.lean "example : False := by { let c : Char := '\"'; sorry }"
+scan_expect 1 lean4/D.lean "def c := '\\\\'  theorem t : True := by sorry"
+scan_expect 1 lean4/D.lean "example : False := by { let c : Char := '\\\"'; sorry }"
+# An escaped quote does not end a string.
+scan_expect 1 lean4/D.lean "def s := \"a\\\"b\" theorem t : True := by sorry"
+# A prime is not a character literal, so the string after it stays a string.
+# Coq has no character literals at all.
+scan_expect 1 coq/C.v "Check (f'\"'\"). Lemma bad : False. Admitted."
+scan_expect 1 lean4/D.lean "def f' := \"'\" theorem t : True := by sorry"
+scan_expect 1 agda/A.agda "f α' = \"'\" ; postulate p : Set"
+# In Agda, `--` straight after an ellipsis opens a comment.
+scan_expect 0 agda/A.agda 'f x ...-- postulate is only a word here'
+# In Agda, `--` inside an identifier does not start a comment.
+scan_expect 1 agda/A.agda 'f--g = x ; postulate p : Set'
+# Escape hatches are per language: `admit` is an ordinary Agda identifier.
+scan_expect 0 agda/A.agda 'admit : Set'
+scan_expect 1 coq/C.v 'Lemma l : True. admit. Qed.'
+
+# A proof directory that is a symbolic link is copied as its contents.
+rm -rf "$work/linked" "$work/real"; mkdir -p "$work/linked" "$work/real"
+printf '%s\n' 'Lemma l : True. Admitted.' > "$work/real/C.v"
+ln -s ../real "$work/linked/coq"
+run 1 "$work/sysbin" --proofs-dir "$work/linked" scan
+grep -q 'escape hatch in coq/C.v' "$work/out" || fail "linked proof directory not scanned"
+
+# Usage errors.
+run 2 "$work/sysbin" bogus-leg
+run 2 "$work/sysbin" --proofs-dir "$work/missing" scan
+
+echo 'PASS: proof-check invocations, exit codes and comment-aware scan'
diff --git a/tools/proof-toolchain/DESIGN.adoc b/tools/proof-toolchain/DESIGN.adoc
index 9344108..9d342da 100644
--- a/tools/proof-toolchain/DESIGN.adoc
+++ b/tools/proof-toolchain/DESIGN.adoc
@@ -167,7 +167,7 @@ plus the supporting tools the mapped provers need.
 |===
 |Role |Tools
 
-|`policy:rust` |Creusot (with Why3 and Why3find)
+|`policy:rust` |Creusot (with Why3 and Why3find) and Verus, the default Rust toolset since the owner ruling of 2026-11-07 (PROOF-POLICY §1.2). Pearlite is Creusot's contract language, not a separate tool. Verus pins its own Z3, which the lock records separately from the `backend` Z3.
 |`policy:ada` |gnatprove (SPARK)
 |`policy:engineering` |Idris2 (with pack)
 |`policy:theory-source` |Agda with its standard library. The standard libraries are their own entries, so the bundle fetches, pins and hashes them like any other input. Two versions side by side, 2.6.3 and 2.6.4.3, because the theory repos pin both; a repo selects its own.
@@ -175,7 +175,7 @@ plus the supporting tools the mapped provers need.
 |`transport` |agda2dedukti, Dedukti (`dkcheck`), Lambdapi. agda2dedukti tracks particular Agda versions; the manifest records which Agda it accepts.
 |`exception:rust` |Kani; Aeneas with Charon (PROOF-POLICY §4.1)
 |`exception:recorded` |TLA+ (`tlc`); Isabelle, HOL Light, HOL4, ACL2, Mizar and PVS (supplementary only). The last five were added 2026-10-27 so a kit-provisioned environment can serve every backend in echidna's default core set. PVS is built from its BSD-3-Clause sources on the bundled SBCL; SRI's click-through licence covers only its Allegro build, which the bundle does not use.
-|`runtime` |Rust toolchains (rustup, the toolchains Creusot and Kani pin), a Java runtime for the `tlc` launcher, the OCaml switch HOL Light runs in, Poly/ML for HOL4 and SBCL for ACL2 and PVS, bundled rather than taken from the host
+|`runtime` |Rust toolchains (rustup, the toolchains Creusot, Kani and Verus pin), a Java runtime for the `tlc` launcher, the OCaml switch HOL Light runs in, Poly/ML for HOL4 and SBCL for ACL2 and PVS, bundled rather than taken from the host
 |`backend` |Z3, CVC5, Yices, Alt-Ergo, E prover, Vampire
 |===
 
@@ -198,6 +198,44 @@ that shares the name; the manifest names it `echidna-solidity` if it stays.
 * *Recheck records* (the echidna hand-off of 2026-10-26) can cite the lock's
   translator and prover versions by hash, which answers "which agda2dedukti,
   which Agda" for every transported leg.
+* *Mathesis* catalogues proof receipts and derives Proof Witness Grades from
+  them (PROOF-POLICY §8). A receipt that cites a lock entry's version and
+  hash answers its "checker and version" field without guessing.
+
+[[deviations]]
+== Deviation records (PROOF-POLICY §6)
+
+PROOF-POLICY §6 names the Guix manifest and the repository's container as
+the routes for proof toolchains in CI. Any other route needs a `deviation`
+record, and most of the bundle is another route: release assets, opam,
+cargo and source builds. So the installer may not ship without these
+records:
+
+* The bundle build writes one deviation record into the lock for each entry
+  it builds other than through Guix or the container. The build owns the lock,
+  so the records are written where the lock is written, not on the host that
+  later installs it. Each record names the leg or obligation the entry
+  serves, the tool, the version it asserts, the digest of what was built,
+  why Guix or the container could not be used, and its state (`open`, or
+  `closed` with the change that closed it).
+* `provers.sh install` copies the lock it checked the bundle against to
+  `$PREFIX/toolchain.lock.json`, beside the unpacked bundle, so the records
+  travel with what was installed. The lock is never inside the bundle: it
+  holds the bundle's own SHA-256. A read-only checkout with a writable prefix
+  is enough; the installer writes nothing back into a repository.
+* Every consuming repository copies the records for the entries it uses into
+  both its proof-status file and the workflow that installs the bundle, as
+  PROOF-POLICY §6 requires. Where it uses an entry for an obligation the
+  record does not name, it adds that obligation and its own reason in both
+  places; the tool, version and digest still come from the lock.
+* The run asserts each tool's version and fails on a mismatch, as `doctor`
+  already does against the lock.
+
+Today nothing installs the bundle, so no deviation is open; this repository's
+`docs/status/PROOF-STATUS.adoc` says so. The exemption follows the route, not
+the tool. A tool installed through the Guix manifest or the container needs
+no record. The same tool installed from the bundle needs one, even if Guix
+also carries it.
 
 [[plan]]
 == Build plan (stacked PRs)
diff --git a/tools/proof-toolchain/toolchain.kyaml b/tools/proof-toolchain/toolchain.kyaml
index bb84eaa..caa1ddd 100644
--- a/tools/proof-toolchain/toolchain.kyaml
+++ b/tools/proof-toolchain/toolchain.kyaml
@@ -22,10 +22,12 @@
   prefix: "/opt/hyperpolymath/provers",
   policy: "standards 3-practice/PROOF-POLICY.adoc",
   tools: [
-    {id: "rust", role: "runtime", method: "rustup into the prefix (toolchains named by Creusot's and Kani's rust-toolchain files)", pin: ["from creusot rust-toolchain", "from kani rust-toolchain"], verify: "rustup run $TOOLCHAIN cargo --version", notes: "every toolchain Creusot and Kani pin is installed; neither uses a host Rust. rustup is set never to install a toolchain on demand, so a missing one fails instead of being fetched", toolchains: "enumerated in the lock from the creusot and kani rust-toolchain files"},
+    {id: "rust", role: "runtime", method: "rustup into the prefix (toolchains named by Creusot's, Kani's and Verus's rust-toolchain files)", pin: ["from creusot rust-toolchain", "from kani rust-toolchain", "from verus release"], verify: "rustup run $TOOLCHAIN cargo --version", notes: "every toolchain Creusot, Kani and Verus pin is installed; none uses a host Rust. rustup is set never to install a toolchain on demand, so a missing one fails instead of being fetched", toolchains: "enumerated in the lock from the creusot and kani rust-toolchain files and the toolchain the verus release names"},
     {id: "creusot", role: "policy:rust", method: "cargo (Creusot INSTALL script, pinned nightly)", pin: "resolve", verify: "cargo creusot --version", needs: ["rust", "why3", "why3find", "z3", "cvc5", "alt-ergo"]},
     {id: "why3", role: "policy:rust", method: "opam", pin: "from creusot creusot-deps.opam", verify: "why3 --version"},
     {id: "why3find", role: "policy:rust", method: "opam", pin: "from creusot creusot-deps.opam", verify: "why3find --help", version: "why3find --version"},
+    {id: "verus", role: "policy:rust", method: "release asset (verus-lang/verus weekly point release, x86-linux zip; Ubuntu 24.04 x86_64 is a prebuilt tier)", pin: "resolve-stable", verify: "verus --version", needs: ["rust", "verus-z3"], notes: "default Rust verifier beside Creusot since the owner ruling of 2026-11-07 (PROOF-POLICY §1.2). It runs on the Rust toolchain its release names, installed through the rust entry. It pins its own Z3, which is the verus-z3 entry; the backend z3 entry is not substituted for it. Pearlite is Creusot's contract language, not a separate tool, so it has no entry"},
+    {id: "verus-z3", role: "runtime", method: "release asset (the Z3Prover/z3 build that the pinned Verus revision's source/tools/get-z3.sh names, installed beside verus where it looks for it)", pin: "from verus source/tools/get-z3.sh", verify: "$PREFIX/verus/z3 --version", notes: "kept apart from the backend z3 entry because Verus checks for its exact Z3 version; get-z3.sh named 4.16.0 on 2026-11-09. The lock records its version and sha256 like any other entry"},
     {id: "gnatprove", role: "policy:ada", method: "release asset (alire-project/GNAT-FSF-builds)", pin: "14.1.0-1", verify: "gnatprove --version"},
     {id: "idris2", role: "policy:engineering", method: "pack (Chez Scheme bootstrap)", pin: "0.8.0", verify: "idris2 --version"},
     {id: "agda-2.6.3", role: "policy:theory-source", method: "cabal into its own store ($PREFIX/agda/2.6.3), exposed only as the wrapper bin/agda-2.6.3", pin: "2.6.3", verify: "agda-2.6.3 --version", notes: "echo-types, ordinal-notation. Their CI pins stdlib v2.3, which upstream lists for Agda 2.8 (it lists 1.7.2/1.7.3 for 2.6.3); the bundle build must type-check each repo against the stdlib it pins before release"},
diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc
index 771b37c..37da671 100644
--- a/verification/proofs/README.adoc
+++ b/verification/proofs/README.adoc
@@ -1,59 +1,59 @@
 = Formal Verification Proofs
 // SPDX-License-Identifier: CC-BY-SA-4.0
 
-This directory contains formal proofs organised by proof assistant.
+The files here are RSR template material. They prove nothing about this
+repository, which has no first-party proof obligations; see
+`docs/status/PROOF-STATUS.adoc`. The estate
+https://github.com/metadatastician/standards/blob/main/3-practice/PROOF-POLICY.adoc[PROOF-POLICY]
+decides which prover carries which obligation.
 
-== Directory Structure
+== Directory structure
 
 [source]
 ----
 proofs/
-├── idris2/          # Idris2 proofs (ABI, dependent types)
-│   ├── ABI/         # ABI-specific proofs (mandatory)
-│   │   ├── Pointers.idr    # Non-null pointer safety
-│   │   ├── Layout.idr      # Memory layout correctness
-│   │   ├── Platform.idr    # Platform type size proofs
-│   │   ├── Foreign.idr     # FFI return type proofs
-│   │   └── Compliance.idr  # C ABI compliance
-│   └── Types.idr    # Core data type well-formedness
-├── lean4/           # Lean4 proofs (algebra, lattices)
+├── idris2/          # Idris2 (APIs, ABIs, engineering properties)
+│   ├── ABI/         # template ABI proofs
+│   └── Types.idr
+├── lean4/           # Lean 4 (a recheck leg for Agda theory)
 │   └── ApiTypes.lean
-├── agda/            # Agda proofs (induction, metatheory)
+├── agda/            # Agda (theory; the source of truth)
+│   ├── bofj-kitt-proofs.agda-lib   # depends on standard-library
 │   └── Properties.agda
-├── coq/             # Coq proofs (type systems, compilation)
+├── coq/             # Rocq/Coq (a recheck leg for Agda theory)
 │   └── TypeSafety.v
-└── tlaplus/         # TLA+ specs (distributed protocols)
+└── tlaplus/         # TLA+ (a §4 exception; a model check is TESTED)
     └── StateMachine.tla
 ----
 
-== Verification Commands
+== Checking
 
 [source,bash]
 ----
-just proof-check-all       # Run all proof checkers
-just proof-check-idris2    # Idris2 only
-just proof-check-lean4     # Lean4 only
-just proof-check-agda      # Agda only
-just proof-check-coq       # Coq only
+just proof-check-all       # every leg, then the escape-hatch scan
+just proof-check-idris2
+just proof-check-lean4
+just proof-check-agda      # agda --safe --without-K --cubical-compatible
+just proof-check-coq
+just proof-scan-dangerous
 ----
 
-== Banned Patterns
+The recipes call `scripts/proof-check.sh`. A missing checker is reported
+`UNAVAILABLE` and the run exits 3; it is never counted as a pass. Checkers
+run on a temporary copy, so no build artefacts are written here. If the
+Agda standard library is not a registered library, set `AGDA_STDLIB` to its
+source directory. TLA+ is not checked by any recipe.
 
-The following MUST NOT appear in any proof file:
+== Escape hatches
 
-- `believe_me` (Idris2)
-- `assert_total` (Idris2)
-- `postulate` (Idris2/Agda)
-- `sorry` (Lean4)
-- `Admitted` (Coq)
-- `unsafeCoerce` (Haskell)
+The scan fails on `believe_me`, `assert_total`, `postulate`, Agda's
+termination pragmas, `sorry`, `admit`, `Admitted`, `unsafeCoerce` and
+`Obj.magic` in proof code. Comments and strings are ignored. The full table
+is in `docs/status/PROOF-NEEDS.adoc`.
 
-CI enforces this via `panic-attack assail --proofs-only`.
+== Adding a proof
 
-== Adding New Proofs
-
-1. Choose the appropriate prover (see PROOF-NEEDS.md)
-2. Create the `.idr`/`.lean`/`.agda`/`.v`/`.tla` file in the right directory
-3. Ensure `%default total` (Idris2) or equivalent
-4. Run the verification command
-5. Update PROOF-STATUS.md
+. Pick the prover PROOF-POLICY §1 maps the obligation to.
+. Add the file under the matching directory.
+. Run its `just proof-check-*` recipe and the scan.
+. Record the obligation and its §5 status in `docs/status/PROOF-STATUS.adoc`.
diff --git a/verification/proofs/agda/bofj-kitt-proofs.agda-lib b/verification/proofs/agda/bofj-kitt-proofs.agda-lib
new file mode 100644
index 0000000..818693c
--- /dev/null
+++ b/verification/proofs/agda/bofj-kitt-proofs.agda-lib
@@ -0,0 +1,3 @@
+name: bofj-kitt-proofs
+depend: standard-library
+include: .