@@ -1,14 +1,14 @@
 ## Machine-Readable Artefacts
 
-The following files in `.machine_readable/descriptiles/` contain structured
-project metadata (a2ml is TOML-flavoured, not Guile Scheme):
+A2ML is retired (standards D99, D269c, D312, D313). The old `.a2ml` sources are
+archived under `archive/a2ml-v1/` and must not be recreated or extended. Use:
 
-- `STATE.a2ml` - Current project state and progress
-- `META.a2ml` - Architecture decisions and development practices
-- `ECOSYSTEM.a2ml` - Position in the ecosystem and related projects
-- `AGENTIC.a2ml` - AI agent interaction patterns
-- `NEUROSYM.a2ml` - Neurosymbolic integration config
-- `PLAYBOOK.a2ml` - Operational runbook
+- `absolute-zero_chora.deed` - project metadata (state, ecosystem, agentic and
+  policy clauses). Deed grammar; validate with the estate deed linter.
+- `.machine_readable/contractiles/<verb>/<verb>.k9.ncl` - the six contracts
+  (must, trust, dust, bust, adjust, intend). The four Hunt contracts are unsigned
+  and must not run as Hunt until signed (ledger K-1).
+- `coordination.k9` - coordination metadata (repo root).
 
 ---
 
@@ -29,7 +29,7 @@ project metadata (a2ml is TOML-flavoured, not Guile Scheme):
 | **Bash/POSIX Shell** | Scripts, automation | Keep minimal |
 | **JavaScript** | Only where AffineScript cannot, or as per-language reference (examples/) | Avoid for new code unless integrating an external JS API |
 | **Nickel** | Configuration language | For complex configs |
-| **Guile Scheme** | Scripting where needed | (state/meta files are `.machine_readable/descriptiles/*.a2ml`, TOML-flavoured) |
+| **Guile Scheme** | Scripting where needed | (metadata is `<repo>_chora.deed`; contracts are `*.k9.ncl`; see Machine-Readable Artefacts) |
 | **Julia** | Batch scripts, data processing | Per RSR |
 | **OCaml** | AffineScript compiler | Language-specific |
 | **Ada** | Safety-critical systems | Where required |
 
@@ -0,0 +1,23 @@
+# SPDX-License-Identifier: MPL-2.0
+# CodeRabbit configuration. Schema: https://coderabbit.ai/integrations/schema.v2.json
+#
+# Ruling D217: CodeRabbit does not push commits to PR branches. Bot commits on a
+# PR branch are unsigned and fail the estate signed-commit floor. Docstrings,
+# fix_ci and resolve_merge_conflict finishing touches are disabled here.
+# The matching app-UI settings must also be off; they live outside
+# this repo and are tracked in the ULTRAPLAN.
+#
+# The docstring pre-merge check stays advisory (mode: warning), as in
+# rsr-template-repo. CodeRabbit is advisory.
+reviews:
+  pre_merge_checks:
+    docstrings:
+      mode: warning
+      threshold: 80
+  finishing_touches:
+    docstrings:
+      enabled: false
+    fix_ci:
+      enabled: false
+    resolve_merge_conflict:
+      enabled: false
@@ -1,23 +1,15 @@
 # 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.
 # Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 #
-# Proof verification CI. Runs the LIGHTWEIGHT provers that are fast and reliable
-# on a standard GitHub runner — Coq (both pillars, all 14 theories), Agda (CNO +
-# OND), and Z3 (CNO + OND bounded instances). Each is an INDEPENDENT job, so one
-# flaking never blocks the others.
+# Proof verification CI for the ACTIVE proof stack (owner ruling 2026-10-10):
+#   * Agda      — CNO + OND + EchoBridge (--safe --without-K)
+#   * Z3        — CNO + OND bounded checks (expect-annotated)
+#   * Idris 2   — the ABI package (absolute-zero-abi.ipkg)
+# Each is an INDEPENDENT job, so one flaking never blocks the others.
 #
-# The Mathlib-free Lean core (CNO, OND, CNOCategory, CNOBridge, FilesystemCNO,
-# LambdaCNO) is built here too, with the toolchain pinned in
-# proofs/lean4/lean-toolchain, and proofs/lean4/AxiomAudit.lean pins the
-# signature of every axiom and the axiom list of every theorem (issue #125).
-#
-# The heavy provers (Lean + multi-GB Mathlib for QuantumCNO/StatMech, Isabelle
-# ~1.2 GB, Mizar i386 + MML, Idris 2 from source) are NOT run here — they are
-# covered by the local/container gate `proofs/verify-all-provers.sh`
-# (ALL-PROVERS-GREEN). See PROOF-STATUS.adoc.
+# Coq, Lean 4, Isabelle/HOL and Mizar are ARCHIVED under archive/proofs/ and are
+# not gated here. See archive/README.adoc for the archive and its status.
 name: Proofs
 
 on:
@@ -26,11 +18,14 @@ on:
   pull_request:
     paths:
       - 'proofs/**'
+      - 'src/**'
+      - 'scripts/check-proof-patterns.sh'
+      - 'tests/check-proof-patterns.sh'
+      - '.machine_readable/contractiles/trust/trust.k9.ncl'
       - 'absolute-zero-abi.ipkg'
       - '.github/workflows/proofs.yml'
       - 'Justfile'
       - '*.agda-lib'
-      - 'lakefile*'
 
 permissions:
   contents: read
@@ -41,37 +36,16 @@ concurrency:
   cancel-in-progress: true
 
 jobs:
-  coq:
-    name: Coq — CNO + OND (14 theories)
+  proof-patterns:
+    name: Proof escape-hatch baseline
     runs-on: ubuntu-24.04
     steps:
       - uses: actions/checkout@v7.0.1
-      - name: Install Coq
-        run: sudo apt-get update && sudo apt-get install -y coq
-      - name: Build all theories via coq_makefile
-        working-directory: proofs/coq
-        run: |
-          coqc --version
-          coq_makefile -f _CoqProject -o Makefile.all
-          make -f Makefile.all -j"$(nproc)"
-          echo "✓ Coq: 14/14 theories compiled (CNO + OND)"
-      - name: Print Assumptions gate (17 named theorems closed) + control
-        working-directory: proofs/coq
-        run: |
-          bash check-assumptions.sh
-          bash check-assumptions.sh --control
-      - name: Axiom tag grammar gate + control (issue #171)
-        working-directory: proofs/coq
-        run: |
-          bash check-axiom-tags.sh
-          bash check-axiom-tags.sh --control
-      - name: Axiom dependency census (issue #171)
-        working-directory: proofs/coq
-        run: |
-          bash census-assumptions.sh
+      - run: bash scripts/check-proof-patterns.sh
+      - run: bash tests/check-proof-patterns.sh
 
   agda:
-    name: Agda — CNO + OND
+    name: Agda — CNO + OND + EchoBridge
     runs-on: ubuntu-24.04
     timeout-minutes: 25
     steps:
@@ -114,25 +88,18 @@ jobs:
           z3 --version
           bash proofs/z3/verify.sh
           echo "✓ Z3: every (check-sat) verdict matched its ; expect annotation"
-      - name: Gate self-test (stub provers + z3 mutants must turn the gate red)
-        run: bash proofs/tests/gate-selftest.sh
 
-  lean:
-    name: Lean — core CNO (6 modules + axiom audit)
-    runs-on: ubuntu-24.04
-    timeout-minutes: 20
+  idris:
+    name: Idris 2 — ABI package (absolute-zero-abi.ipkg)
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    container:
+      # Same pinned idris2-pack image as pages.yml (digest-pinned).
+      image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff
     steps:
       - uses: actions/checkout@v7.0.1
-      - name: Install elan v4.2.4 (sha256-verified) and the pinned toolchain
-        # elan is fetched as a release tarball and checksum-verified rather than
-        # via a third-party action, so the repo's Actions allow-list is not in
-        # play. The toolchain itself comes from proofs/lean4/lean-toolchain.
+      - name: Build the ABI package (type-checks every src/abi module)
         run: |
-          curl -fsSL --retry 3 -o elan.tgz \
-            https://github.com/leanprover/elan/releases/download/v4.2.4/elan-x86_64-unknown-linux-gnu.tar.gz
-          echo "42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63  elan.tgz" | sha256sum -c -
-          tar -xzf elan.tgz
-          ./elan-init -y --no-modify-path --default-toolchain none
-          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
-      - name: Build the six Mathlib-free modules and run the axiom audit
-        run: bash proofs/lean4/check-core.sh
+          idris2 --version
+          idris2 --build absolute-zero-abi.ipkg
+          echo "✓ Idris 2: absolute-zero-abi.ipkg builds"
@@ -46,20 +46,6 @@ build:affinescript:
 # Verification Stage
 # ============================================================================
 
-verify:coq:
-  stage: verify
-  image: coqorg/coq:latest
-  script:
-    - cd proofs/coq/common
-    - coqc CNO.v
-    - cd ../malbolge
-    - coqc -R ../common CNO MalbolgeCore.v
-  artifacts:
-    paths:
-      - proofs/coq/**/*.vo
-    expire_in: 1 day
-  allow_failure: false
-
 verify:z3:
   stage: verify
   image: ubuntu:22.04
@@ -70,26 +56,6 @@ verify:z3:
     - z3 cno_properties.smt2
   allow_failure: false
 
-verify:lean4:
-  stage: verify
-  image: leanprover/lean4:latest
-  script:
-    - cd proofs/lean4
-    - lake build
-  artifacts:
-    paths:
-      - proofs/lean4/.lake/
-    expire_in: 1 day
-  allow_failure: true  # Lean 4 may not be fully set up
-
-verify:isabelle:
-  stage: verify
-  image: makarius/isabelle:latest
-  script:
-    - isabelle build -D proofs/isabelle
-  allow_failure: true  # Isabelle setup may vary
-
-# ============================================================================
 # Test Stage
 # ============================================================================
 
@@ -140,10 +106,8 @@ verify:summary:
     - echo "=========================================="
     - echo "Multi-Prover Verification Summary"
     - echo "=========================================="
-    - echo "Coq:      ✓ (if verify:coq passed)"
     - echo "Z3:       ✓ (if verify:z3 passed)"
-    - echo "Lean 4:   ⚠ (if verify:lean4 passed, else optional)"
-    - echo "Isabelle: ⚠ (if verify:isabelle passed, else optional)"
+    - echo "Coq, Lean 4, Isabelle: archived under archive/proofs/ (retired 2026-10-10; not gated)"
     - echo ""
     - echo "Multi-prover agreement increases confidence!"
   when: always
 
@@ -1,6 +1,9 @@
 // SPDX-License-Identifier: CC-BY-SA-4.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = bot_directives — per-repo directives for automated agents
+
+NOTE: Retired 2026-10-10. The A2ML files described below are archived under `archive/a2ml-v1/` (see `archive/a2ml-v1/MIGRATION-LEDGER.adoc`). Repository metadata now lives in `absolute-zero_chora.deed`, and contracts live in `.machine_readable/contractiles/<verb>/<verb>.k9.ncl`. The text below describes the retired set and is kept as history until it is rewritten.
+
 :toc:
 
 == Purpose