hyperpolymath · Oct 9, 2026 · Oct 9, 2026 · Oct 9, 2026 · Oct 9, 2026 · coderabbitai
@@ -9,7 +9,7 @@ type = "state-file"
 [metadata]
 project = "echidna"
 version = "2.3.0"
-last-updated = "2026-06-13"
+last-updated = "2026-10-09"
 status = "active"
 release-tag = "v2.3.0"
 
@@ -18,6 +18,17 @@ name = "echidna"
 completion-percentage = 100
 phase = "v2.3.0 Released — saturation+typing (#198) + GNN training wiring (#207) + dispatcher all-17-adapters (PR pending SPDX hook) + comprehensive contractile family (#214) + first owner-authorised GNN training run completed (best MRR 0.92)"
 
+[session-2026-10-09-deed-baseline]
+summary = "Deed-era baseline landed; STATE refreshed past the 2026-10-05 integrations wave"
+changes = [
+  "Recorded the integrations wave that postdated the last STATE touch (2026-06-13): echidna prove --output json emitting echidna.prove.result/1 (JCS-canonical I-JSON), echidna-core 0.2.0 consumable by echidnabot + proof-burrower, echidna-core-spark renamed echidna-core-creusot with the trust kernel re-exported as echidna_core::trust, ffi/zig building and CI-gated (zig-ffi-ci.yml) — all in CHANGELOG.adoc [Unreleased]",
+  "New echidna_chora.deed at repo root: first deed under the one-deed-per-repo doctrine (standards#837), translated from CLADE.a2ml (family 1) and ECOSYSTEM.a2ml (family 2) per standards 1-formats/deed/mappings/; clade names verbatim from gv-clade-index verisim/seed/clades.a2ml; passes deed_lint (deed.abnf)",
+  "Fail-closed, per the mapping frame: no (meta …) clause yet — this repo's META.a2ml predates the family-2 field table; STATE (family 3) and 0-AI-MANIFEST (family 7) translations stay owner-pending in standards",
+  "The ten stale AGPL-3.0-or-later SPDX headers under HOL-o-extension/, audits/ and training_data/ were left in place by design: D262's recorded plan (CHANGELOG [Unreleased], docs/DEBT.adoc P0) rewrites them inside the a2ml->deed conversion, so this baseline does not touch an owner-gated licensing surface early",
+  "0-AI-MANIFEST.a2ml drift fixed: full-version 1.6.0 -> 2.3.0, UI runtime Deno -> Bun (Deno banned estate-wide 2026-09-22), deed added to canonical-locations",
+]
+consumers-note = ".machine_readable descriptiles stay until their consumers move to the deed; until then identity/status changes go in both places"
+
 [session-2026-06-13-dogfood-proof-ci]
 summary = "Proof corpus repaired and gated in CI (PR #234, squash-merged to main 2026-06-06)"
 pr = "https://github.com/hyperpolymath/echidna/pull/234"

diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml
@@ -10,7 +10,7 @@
 version = "1.1"
 project = "echidna"
 type = "neurosymbolic-theorem-prover"
-full-version = "1.6.0"
+full-version = "2.3.0"
 license = "MPL-2.0"
 author = "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"
 repo = "https://github.com/hyperpolymath/echidna"
@@ -31,6 +31,7 @@ repo = "https://github.com/hyperpolymath/echidna"
 #   node_modules/    — dependencies
 
 [canonical-locations]
+deed = "echidna_chora.deed"
 state-files = ".machine_readable/"
 state = ".machine_readable/descriptiles/STATE.a2ml"
 meta = ".machine_readable/descriptiles/META.a2ml"
@@ -47,7 +48,7 @@ container = "container/"
 
 [tech-stack]
 primary = "Rust (141 ProverKind variants over 105 backend implementations — see docs/PROVER_COUNT.adoc; trust pipeline, CLI, REPL, API servers)"
-secondary = "Julia (ML inference, port 8090), AffineScript+Deno (UI, 33 files, zero TypeScript)"
+secondary = "Julia (ML inference, port 8090), AffineScript+Bun (UI, TEA architecture, zero TypeScript; Deno banned estate-wide 2026-09-22)"
 optional = "Chapel (parallel proof dispatch)"
 abi = "Idris2 (7 modules, zero believe-me)"
 ffi = "Zig (4 shared libraries)"

diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc
@@ -41,6 +41,28 @@ kernel tests never ran in CI.
 is a hard gate or that milestones 8c-M1..M3 are done; it records why
 Creusot does not run in CI.
 
+==== Added — governance 2026-10-09
+
+* *`+echidna_chora.deed+`* at the repo root: the first deed under the
+estate one-deed-per-repo doctrine (standards#837), translated from
+`+CLADE.a2ml+` (family 1) and `+ECOSYSTEM.a2ml+` (family 2) per the
+standards `+1-formats/deed/mappings/+` frame, following the
+`+proof-burrower_chora.deed+` precedent; clade names verbatim from the
+gv-clade-index taxonomy seed; passes the normative `+deed.abnf+`
+validator. The `+.a2ml+` descriptiles stay until their consumers move;
+identity/status edits touch both surfaces until then (noted in the deed
+header).
+
+==== Fixed — governance 2026-10-09
+
+* `+0-AI-MANIFEST.a2ml+`: `+full-version+` was frozen at a stale 1.x
+value; it now tracks `+Cargo.toml+`. The UI runtime line reads Bun
+(Deno was banned estate-wide 2026-09-22; JS-RUNTIME-POLICY), and the
+deed is listed under `+[canonical-locations]+`.
+* `+.machine_readable/descriptiles/STATE.a2ml+`: refreshed past the
+2026-10-05 integrations wave and recorded the deed baseline (session
+protocol).
+
 ==== Changed
 
 * *Licence: `+AGPL-3.0-or-later+` → `+MPL-2.0+` for code and the

diff --git a/echidna_chora.deed b/echidna_chora.deed
@@ -0,0 +1,82 @@
+;; SPDX-License-Identifier: MPL-2.0
+;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+;
+; The repo deed of echidna (one-deed-per-repo doctrine, standards#837).
+; Scope of this first deed (2026-10-09): identity, clade, forges, lineage
+; and status translated from .machine_readable/CLADE.a2ml (family 1), plus
+; the ecosystem clause translated from .machine_readable/descriptiles/
+; ECOSYSTEM.a2ml (family 2), per standards 1-formats/deed/mappings/
+; clade-to-repo-deed.adoc and meta-ecosystem-to-repo-deed.adoc. Clade
+; names follow gv-clade-index verisim/seed/clades.a2ml verbatim.
+;
+; Not translated (fail-closed, per the mapping frame):
+;  - the (meta ...) clause: echidna's META.a2ml predates the family-2
+;    field-table shape and needs a table-extension review first
+;  - ECOSYSTEM.a2ml [deployment], [corpus-sources], [vocab-sources],
+;    [proof-exchange-standards] and [self-proof-ci]: not in the family-2
+;    table, so they stay in ECOSYSTEM.a2ml
+;  - STATE.a2ml (family 3) and 0-AI-MANIFEST.a2ml (family 7): owner
+;    decisions pending in standards (state-v1-decision.adoc,
+;    ai-manifest-decision.adoc); nothing here pre-empts them
+; The .a2ml surfaces above are still read by consumers (session protocol,
+; openssf-compliance, contractiles Justfile), so they stay until their
+; consumers move to this deed; until then a change to identity or status
+; must be made in both places.
+;
+; Deviations recorded: CLADE.a2ml [lineage] parent carried a description
+; ("Neurosymbolic theorem proving - neural proof synthesis") although the
+; lineage type is standalone; the deed carries "" per the parent-is-the-
+; monorepo-parent-never-a-description doctrine. The status history note
+; was the clade-status-backfill placeholder; it is re-derived here.
+(repo-deed
+  :schema-version "1.0.0"
+  :canonical-name "echidna"
+  :beholding-chora #u5"estate/chora"
+  :repo-uuid #u5"github.com/hyperpolymath/echidna"
+
+  (identity :primary-forge github
+            :owner "hyperpolymath"
+            :prefixed-name "fv-echidna")
+
+  (clade :primary fv
+         :primary-name "Formal Verification & Proofs"
+         :secondary (ax)
+         :assigned "2026-03-16"
+         :rationale "")
+
+  (forges :github "hyperpolymath/echidna"
+          :gitlab "hyperpolymath/echidna"
+          :bitbucket "hyperpolymath/echidna")
+
+  (lineage :type standalone
+           :parent ""
+           :born "2026-03-16"
+           :previous-names ())
+
+  (status :phase active
+          :since "2026-03-16"
+          :present #t
+          :aliases ()
+          :merged-into ""
+          :superseded-by ""
+          :successors ()
+          :ended ""
+          (history
+            (entry :phase active
+                   :since "2026-03-16"
+                   :note "trust-hardened neurosymbolic theorem prover; proving core of the hyperpolymath estate")))
+
+  (ecosystem :project "echidna"
+             :ecosystem "hyperpolymath"
+             :position-type "component"
+             :purpose "Trust-hardened neurosymbolic theorem proving platform. 141 ProverKind variants across 105 backend implementations, 12 exposed by default at GET /api/provers (Agda, Coq, Lean 4, Isabelle/HOL, Z3, CVC5, Metamath, HOL Light, Mizar, PVS, ACL2, HOL4); canonical tier table and count semantics in docs/PROVER_COUNT.adoc. Sandboxed solver execution (Podman/bubblewrap), proof certificate checking, axiom tracking, GNN-guided proof search, Julia ML inference layer."
+             :coordination ""
+             (related :name "proven-servers (nesy-solver-api)" :relationship consumer :notes "nesy-solver-api calls /api/verify on echidna-nesy.flycast:8090. Cold-start grace 90s.")
+             (related :name "hypatia" :relationship sibling-neurosym :notes "Hypatia performs neurosymbolic CI scanning; echidna does theorem proving. Both are Tier 2 formal verification tools.")
+             (related :name "verisimdb" :relationship active-integration :notes "Corpus emits 8-modality octads (corpus/octad.rs) compatible with /api/v1/octads. Round-trip verified; HTTP push deferred.")
+             (related :name "neural-foundations" :relationship monorepo-satellite :notes "echidna is mirrored as a submodule/satellite inside neural-foundations.")
+             (related :name "maa-framework" :relationship sibling :notes "Absolute-zero and related MA/ML tools in same neurosymbolic tier.")
+             (related :name "echo-types" :relationship active-consumer :notes "Echidna's design-search drove the Phase 1.3 _≤_ redesign + unbudgeted wf-<ᵇʳᶠ rank-function recommendations. Handoff document at echo-types/docs/echidna-design-search-2026-04-28.adoc. 640 entries indexed.")
+             (related :name "januskey/reversible-core" :relationship planned-integration :notes "Bennettian reversibility substrate for the SA annealer trace ledger. Not yet wired.")
+             (related :name "jtv (Lean 4)" :relationship indexed :notes "147 entries verified during Lean adapter rollout.")
+             (related :name "eclexia (Idris 2 ABI)" :relationship indexed :notes "93 entries verified during Idris 2 adapter rollout.")))