docs(6a2): supersede #107 — de-templatize machine_readable + honest STATE + self-validating rename (#114)

Supersedes #107. Brings the parked `test/ci-full-verisimdb` baseline
onto current `main`, scoped to the de-templatization + an
**honesty-corrected STATE**.

## In
- **6a2 refresh** — AGENTIC/ECOSYSTEM/META/NEUROSYM/PLAYBOOK/STATE
de-templatized (NEUROSYM no longer literally says `rsr-template-repo`).
- **`bot_directives/*.scm` → `.a2ml`** (estate convention; matches
vcl-ut — not kept side-by-side).
- **`svc/k9` → `svc/self-validating`** rename.
- `contractiles/dust/Dustfile` filled; README OpenSSF badge.

## STATE honesty (the key correction)
Per a **machine-checked Coq `Print Assumptions` audit** (coqc 8.18),
#107's `formal-proofs: 8/8 closed` was an overclaim. Replaced with
honest per-module status: **0-axiom** C2/V2;
**closed-modulo-standard-primitives** Octad(O/R)/P2/P3/C7; **structural
over uninterpreted ops** D1/D2/N2; **crux axiomatised** Q1
(`optimize_is_permutation`); **no Coq↔Rust refinement link yet**. Also
corrected **`verisim-nif`** `implemented`→`stub` (it returns
`nif_placeholder`, per #61). Proof-debt tracked in #113.

## Excluded (deferred, on purpose)
- The branch's bulk `timeout-minutes` workflow edits — one was
**invalid** (`timeout-minutes` on a reusable-workflow `uses:` caller);
needs a separate correct pass.
- The branch's older pre-consonance 310-line `EXPLAINME` — kept main's
newer 130-line consonance version (the richer evidence-based one can be
folded in later).
- Throwaway `TEST_CI_*` markers — dropped.

https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME

---
_Generated by [Claude
Code](https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/0-AI-MANIFEST.a2ml

@@ -0,0 +1,22 @@
+# AI Manifest for 6a2 Directory
+
+## Purpose
+
+This manifest declares the AI-assistant context for the 6a2 machine-readable metadata directory.
+
+## Canonical Locations
+
+The 6 core A2ML files MUST exist in this directory:
+1. AGENTIC.a2ml
+2. ECOSYSTEM.a2ml
+3. META.a2ml
+4. NEUROSYM.a2ml
+5. PLAYBOOK.a2ml
+6. STATE.a2ml
+
+## Invariants
+
+- No duplicate files in root directory
+- Single source of truth: this directory is authoritative
+- No stale metadata
+

.machine_readable/6a2/AGENTIC.a2ml

@@ -1,16 +1,46 @@
 ;; SPDX-License-Identifier: MPL-2.0
-;; AGENTIC.scm - AI agent interaction patterns for rsr-template-repo
+;; AGENTIC.a2ml - AI agent interaction patterns for VeriSimDB
 
 (define agentic-config
   `((version . "1.0.0")
+    (project . "VeriSimDB")
+
     (claude-code
-      ((model . "claude-opus-4-5-20251101")
-       (tools . ("read" "edit" "bash" "grep" "glob"))
-       (permissions . "read-all")))
+      ((model . "claude-opus-4-7")
+       (tools . ("read" "edit" "bash" "grep" "glob" "agent"))
+       (permissions . "read-all + edit-with-confirmation")))
+
     (patterns
-      ((code-review . "thorough")
-       (refactoring . "conservative")
-       (testing . "comprehensive")))
+      ((code-review . "thorough — verify against EXPLAINME.adoc claims-with-evidence")
+       (refactoring . "conservative — preserve formal-proof invariants in formal/*.v")
+       (testing . "comprehensive — Rust cargo test + Elixir mix test + Coq build-oracle")
+       (licence-edits . "MANUAL ONLY — see feedback_no_automated_licence_edits")
+       (proofs . "MUST check via Print Assumptions; cross-document with echo-types if L3 obligation")))
+
     (constraints
-      ((languages . ())
-       (banned . ("typescript" "go" "python" "makefile"))))))
+      ((languages-allowed . ("Rust" "Elixir" "ReScript" "Coq" "Idris2"))
+       (languages-banned . ("TypeScript" "Go" "Python" "Node.js" "Makefile"))
+       (container-runtime . "Podman > Docker")
+       (source-hosting-preference . "GitLab > GitHub")
+       (licence . "MPL-2.0 — sole-owner repo per estate license-policy umbrella")))
+
+    (load-bearing-memories
+      ((feedback_estate_license_policy_umbrella . "five-way license rule")
+       (feedback_no_automated_licence_edits . "manual licence edits only")
+       (feedback_proofs_must_check_and_cross_doc_echo_types . "proof obligations cross-doc")
+       (project_verisimdb_subject_of_everything . "VCL rename incomplete; ecosystem dependencies")
+       (project_verisimdb_proof_programme_started . "foundation-pack proof status")))
+
+    (canonical-numbers-source
+      ((modality-list . "rust-core/verisim-{graph,vector,tensor,semantic,document,temporal,provenance,spatial}/")
+       (crate-count . "find rust-core -name Cargo.toml -not -path */fuzz/*")
+       (test-counts . "cargo test 2>&1 | grep test result")
+       (proof-count . "ls formal/*.v")
+       (foundation-pack-status . "ROADMAP.md")
+       (drift-type-catalogue . ".claude/CLAUDE.md section Drift Detection")))
+
+    (do-not
+      ((modify-licence-headers-in-bulk . "manual per-file owner-only")
+       (touch-third-party-vendored . "leave fork contents alone")
+       (sweep-cross-repo . "high blast-radius without explicit owner approval")
+       (assume-pre-authorization . "Work-without-stopping is not authorization for forbidden actions")))))

.machine_readable/6a2/ECOSYSTEM.a2ml

@@ -1,20 +1,58 @@
 ;; SPDX-License-Identifier: MPL-2.0
-;; ECOSYSTEM.scm - Ecosystem position for rsr-template-repo
-;; Media-Type: application/vnd.ecosystem+scm
+;; ECOSYSTEM.a2ml - Ecosystem position for VeriSimDB
+;; Media-Type: application/vnd.ecosystem+a2ml
 
 (ecosystem
   (version "1.0")
-  (name "rsr-template-repo")
-  (type "")
-  (purpose "")
+  (name "VeriSimDB")
+  (type "database + federation coordinator")
+  (purpose "Cross-modal entity consistency engine — detects drift before it causes data quality damage; operates standalone or as heterogeneous federation coordinator over existing databases.")
 
   (position-in-ecosystem
-    (category "")
-    (subcategory "")
-    (unique-value ()))
+    (category "multimodal database")
+    (subcategory "drift-aware federation")
+    (unique-value
+      ("Octad: one entity, eight synchronised representations"
+       "Continuous cross-modal drift detection with severity scoring"
+       "Self-normalisation via authoritative-modality selection"
+       "Formally verified consistency obligations (8 Coq modules)"
+       "VCL — formally verified query language with PROOF clauses"
+       "Operates as standalone DB OR federation coordinator over 7 external backends")))
 
-  (related-projects ())
+  (related-projects
+    ;; Direct dependencies (hyperpolymath estate)
+    (("hyperpolymath/echo-types"        "echo / drift / cost-typing foundations (cross-doc target)"))
+    (("hyperpolymath/vcl-ut"             "VCL unification toolchain (formal foundation)"))
+    (("hyperpolymath/tropical-resource-typing" "tropical cost-typing (drift cost composition)"))
+    (("hyperpolymath/kategoria"          "category-theory foundations"))
+    (("hyperpolymath/typed-wasm"         "WASM target for VCL compilation"))
+    (("hyperpolymath/affinescript"       "ReScript-successor language; consumes verisimdb client SDK"))
+    (("hyperpolymath/panll"              "PanLL database protocol; embeds verisimdb-debugger"))
+    ;; Hypatia pipeline (estate observability)
+    (("hyperpolymath/hypatia"            "estate-wide CI/CD scanning; ingests verisim octads"))
+    (("hyperpolymath/panic-attack"       "scan source; emits weak_points to verisimdb-data"))
+    (("hyperpolymath/verisimdb-data"     "git-backed flat-file store for CI scans + dispatch manifests"))
+    (("hyperpolymath/gitbot-fleet"       "dispatch infrastructure; consumes verisimdb octads"))
+    ;; Container ecosystem (estate)
+    (("hyperpolymath/stapeln"            ".ctp container bundle ecosystem; ct-build.sh signing"))
+    (("hyperpolymath/svalinn"            "edge gateway (.gatekeeper.yaml policy)"))
+    (("hyperpolymath/cerro-torre"        "container manifest (manifest.toml provenance)"))
+    (("hyperpolymath/selur"              "selur-compose stack runner"))
+    ;; Formal-proof ecosystem (estate)
+    (("hyperpolymath/ephapax"            "preservation theorem track; cross-doc echo-types target")))
 
-  (what-this-is ())
+  (what-this-is
+    ("A cross-modal consistency engine that detects + repairs drift across eight entity representations"
+     "A multimodal database where one entity ID maps to eight synchronised stores"
+     "A formally verified query layer (VCL) over heterogeneous data"
+     "A federation coordinator over 7 backends: MongoDB / Redis / Neo4j / ClickHouse / SurrealDB / InfluxDB / MinIO"
+     "A reference implementation for PanLL's database design/development/evaluation module"
+     "An octad-emitting source for the hypatia estate CI/CD pipeline"))
 
-  (what-this-is-not ()))
+  (what-this-is-not
+    ("NOT a SQL database — VCL is the query interface; SQL is not supported"
+     "NOT a replacement for any single-modality database — pairs WITH them via federation"
+     "NOT a graph-only DB — graph is one of eight modalities"
+     "NOT a vector-only DB — vector is one of eight modalities"
+     "NOT eventual-consistency — drift detection operates on the semantic layer"
+     "NOT Python / Go / Node.js — banned per language policy in .claude/CLAUDE.md")))

.machine_readable/6a2/META.a2ml

@@ -1,17 +1,72 @@
 ;; SPDX-License-Identifier: MPL-2.0
-;; META.scm - Meta-level information for rsr-template-repo
-;; Media-Type: application/meta+scheme
+;; META.a2ml - Meta-level information for VeriSimDB
+;; Media-Type: application/vnd.meta+a2ml
 
 (meta
-  (architecture-decisions ())
+  (architecture-decisions
+    (("AD-001"
+       (decision "Marr's three levels of analysis as the design lens")
+       (rationale "Computational / algorithmic / implementational separation keeps the octad invariant clean")
+       (source ".claude/CLAUDE.md section 'Design Philosophy'")))
+    (("AD-002"
+       (decision "Rust core + Elixir orchestration split")
+       (rationale "Rust for performance-critical modality stores; Elixir/OTP for distributed coordination + fault tolerance")
+       (source "README.adoc + .claude/CLAUDE.md 'Architecture'")))
+    (("AD-003"
+       (decision "Pluggable storage backend (verisim-storage) with redb as pure-Rust default")
+       (rationale "Eliminate oxrocksdb-sys C++ dependency; Oxigraph feature-flagged")
+       (source "rust-core/verisim-storage + rust-core/verisim-graph")))
+    (("AD-004"
+       (decision "PLONK as ZKP scheme for VCL-DT PROOF clause")
+       (rationale "Universal trusted setup + small proofs + recursion + circuit flexibility (see Trustfile table)")
+       (source "contractiles/trust/Trustfile")))
+    (("AD-005"
+       (decision "Git-backed flat-file store for GitHub CI integration (verisimdb-data repo)")
+       (rationale "No persistent server needed for ~290-repo scanning workflow; verisim-api server runs locally as needed")
+       (source ".claude/CLAUDE.md 'GitHub CI Integration'")))
+    (("AD-006"
+       (decision "MPL-2.0 across the workspace (no AGPL)")
+       (rationale "Sole-owner repo per estate license-policy umbrella")
+       (source "LICENSE + Cargo.toml + PR #101 (closes issue #82)")))
+    (("AD-007"
+       (decision "Tantivy 0.26 with order_by_score() for TopDocs")
+       (rationale "Tantivy 0.26 collector API change; lz4_flex + lru CVE resolution via transitive bump")
+       (source "PR #76 + reference_tantivy_0_26_collector_api memory"))))
 
   (development-practices
-    (code-style ())
+    (code-style
+      ("rustfmt + clippy --all-targets --all-features"
+        "Elixir mix format"
+        "AsciiDoc for prose docs"
+        "a2ml for machine-readable artefacts"))
     (security
-      (principle "Defense in depth"))
-    (testing ())
+      (principle "Defense in depth")
+      (practices
+        ("cargo deny check (advisories + bans + licenses + sources)"
+         "cargo audit (RUSTSEC)"
+         "cargo-llvm-cov coverage gate (>= 60%)"
+         "fuzz targets (Rust + cargo-fuzz)"
+         "OpenSSF Scorecard enforcement"
+         "SHA-pinned actions"
+         "Stapeln container signing + .ctp bundle attestations")))
+    (testing
+      ("Rust: cargo test + integration tests under rust-core/*/tests/"
+       "Elixir: mix test (incl. --include integration for 105 federation-adapter tests via selur-compose stack)"
+       "Coq: formal proofs in formal/*.v with Print Assumptions guard"))
     (versioning "SemVer")
-    (documentation "AsciiDoc")
-    (branching "main for stable"))
+    (documentation "AsciiDoc (README.adoc, EXPLAINME.adoc, contractiles/README.adoc); a2ml for state/meta/ecosystem/agentic/neurosym/playbook")
+    (branching "main for stable; feature branches off main; squash-merge into main"))
 
-  (design-rationale ()))
+  (design-rationale
+    (("rationale-octad"
+       (claim "Eight modalities is not arbitrary")
+       (reasoning "Each modality captures a distinct entity-level semantic: structure (Graph), similarity (Vector), high-dimensional shape (Tensor), type-system intent (Semantic), text content (Document), time (Temporal), origin (Provenance), location (Spatial). Together they span the practical entity-representation space without redundancy.")))
+    (("rationale-drift-vs-eventual-consistency"
+       (claim "Drift detection > eventual consistency for cross-modal data")
+       (reasoning "Eventual consistency cures structural divergence; it does not cure semantic divergence (vector that no longer matches text; provenance hash whose chain is broken). Drift detection + self-normalisation operates at the semantic layer.")))
+    (("rationale-formal-proofs"
+       (claim "Coq proofs for the consistency obligations")
+       (reasoning "Foundation-pack (P2/P3/D1/C2/C7/N2/V2/Q1) covers the invariants that would be expensive to debug empirically: hash-chain integrity, normaliser fixed-points, WAL idempotency, planner semantic equivalence.")))
+    (("rationale-flat-file-ci"
+       (claim "Git-backed flat-file store instead of persistent server in GitHub CI")
+       (reasoning "Persistent server scoped to ~290 repos × per-PR scans would dominate CI cost. Flat-file store keeps the data path read-only-from-git and write-via-repository_dispatch; verisim-api server is opt-in for local dev or future Fly.io deployment.")))))

.machine_readable/6a2/NEUROSYM.a2ml

@@ -1,13 +1,44 @@
 ;; SPDX-License-Identifier: MPL-2.0
-;; NEUROSYM.scm - Neurosymbolic integration config for rsr-template-repo
+;; NEUROSYM.a2ml - Neurosymbolic integration config for VeriSimDB
 
 (define neurosym-config
   `((version . "1.0.0")
+    (project . "VeriSimDB")
+
     (symbolic-layer
-      ((type . "scheme")
+      ((type . "Coq + Idris2 + Scheme/a2ml")
        (reasoning . "deductive")
-       (verification . "formal")))
+       (verification . "formal-proofs")
+       (modules
+         (("formal/Drift.v"          . "drift detection semantics + drift-type taxonomy"))
+         (("formal/Normalizer.v"     . "normalisation procedure + atomicity invariants"))
+         (("formal/Planner.v"        . "query planner cost model"))
+         (("formal/PlannerSemantic.v" . "Q1-full planner semantic equivalence"))
+         (("formal/Provenance.v"     . "P2 + P3 — append_preserves_verified, build_chain_all_verified"))
+         (("formal/Transaction.v"    . "C2 — txn_state_machine (0 axioms)"))
+         (("formal/VCL.v"            . "N2 normalize_idempotent + V2 vql_preservation"))
+         (("formal/WAL.v"            . "C7 wal_replay_idempotent on observable state")))
+       (idris2-bridge
+         ((path . "VQL-DT type checker via Elixir-native + ReScript + Rust ZKP bridge")
+          (proof-types . ("EXISTENCE" "INTEGRITY" "CONSISTENCY" "PROVENANCE" "FRESHNESS"
+                           "ACCESS" "CITATION" "CUSTOM" "ZKP" "PROVEN" "SANCTIFY"))))))
+
     (neural-layer
-      ((embeddings . false)
-       (fine-tuning . false)))
-    (integration . ())))
+      ((embeddings . true)
+       (embeddings-modality . "verisim-vector (HNSW similarity search)")
+       (embedding-source . "user-supplied per Octad input; not generated by VeriSimDB")
+       (tensor-modality . "verisim-tensor via Burn (active research)")
+       (fine-tuning . false)
+       (purpose . "host embeddings + tensors as first-class entity representations; drift detection compares against semantic + document modalities")))
+
+    (integration
+      (neurosym-bridge
+        ((drift-detection . "neural (vector) vs symbolic (semantic / type system) divergence is one of six drift types")
+         (proof-clauses . "VCL queries can carry PROOF clauses that pin entity invariants symbolically")
+         (zkp-bridge . "zkp.rs (367 LOC) + zkp_bridge.rs (628 LOC) + sanctify_bridge.rs (413 LOC) route VCL PROOF obligations through PLONK")
+         (echo-types . "drift cost composition with echo-types and tropical-resource-typing per cross-doc target"))))
+
+    (verification-policy
+      ((coq-build-oracle . "yes — .github/workflows/coq-build.yml")
+       (print-assumptions-guard . "yes — per-theorem 0-axiom asserts on critical modules")
+       (cross-doc-echo-types . "required for L3 obligations per feedback_proofs_must_check_and_cross_doc_echo_types")))))

.machine_readable/6a2/PLAYBOOK.a2ml

@@ -1,13 +1,63 @@
 ;; SPDX-License-Identifier: MPL-2.0
-;; PLAYBOOK.scm - Operational runbook for rsr-template-repo
+;; PLAYBOOK.a2ml - Operational runbook for VeriSimDB
 
 (define playbook
   `((version . "1.0.0")
+    (project . "VeriSimDB")
+
     (procedures
-      ((deploy . (("build" . "just build")
-                  ("test" . "just test")
-                  ("release" . "just release")))
-       (rollback . ())
-       (debug . ())))
-    (alerts . ())
-    (contacts . ())))
+      (build
+        ((rust-only . "cd rust-core && cargo build --release")
+         (full . "cargo build --release && cd elixir-orchestration && mix compile")
+         (container-in-memory . "podman build -t verisimdb:latest -f container/Containerfile .")
+         (container-persistent . "podman build -t verisimdb:persistent --build-arg FEATURES=persistent -f container/Containerfile .")
+         (signed-bundle . "cd container && ./ct-build.sh persistent --push")))
+
+      (test
+        ((rust-unit . "cargo test")
+         (rust-integration . "cargo test --test integration")
+         (elixir-unit . "cd elixir-orchestration && mix test")
+         (elixir-integration . "cd elixir-orchestration && mix test --include integration")
+         (federation-adapters . "cd connectors/test-infra && selur-compose up -d && cd ../../elixir-orchestration && mix test --include integration")
+         (coq-proofs . "cd formal && just check")
+         (fuzz . "cargo fuzz run <target> -- -max_total_time=60")))
+
+      (run
+        ((api-server . "cargo run -p verisim-api -- --bind 127.0.0.1:8080")
+         (elixir-orchestration . "cd elixir-orchestration && iex -S mix")
+         (repl . "cargo run -p verisim-repl")
+         (debugger . "cd debugger && cargo run -- --rust-url http://localhost:8080 --orch-url http://localhost:4080")
+         (full-stack . "selur-compose up --detach")
+         (container-quick . "podman run -p 8080:8080 verisimdb:latest")))
+
+      (deploy
+        ((local . "podman run -p 8080:8080 -v verisimdb-data:/data verisimdb:persistent")
+         (selur-stack . "cd container && selur-compose up --detach")
+         (github-ci-scan . "via verisimdb-data repository_dispatch from per-repo scan-and-report.yml")))
+
+      (rollback
+        ((via-stapeln . "verify .ctp bundle attestation before re-launch")
+         (via-git . "git revert <bad-commit> && cargo deny check && cargo test")
+         (via-wal-replay . "verisim-wal replay; idempotency proven by C7")))
+
+      (debug
+        ((interactive-tui . "cd debugger && cargo run -- --rust-url http://localhost:8080")
+         (panll-protocol . "JSON-over-stdio: {\"cmd\":\"inspect\",\"entity_id\":\"...\"}")
+         (drift-scan . "{\"cmd\":\"drift_scan\",\"threshold\":0.3}")
+         (vql-trace . "{\"cmd\":\"trace_vql\",\"query\":\"SELECT ...\"}")
+         (proof-verify . "{\"cmd\":\"verify_proof\",\"query\":\"... PROOF ...\"}")
+         (health . "{\"cmd\":\"health\"}")
+         (formal-proof-check . "cd formal && coqc -Q . VeriSimDB <Module>.v && Print Assumptions <Theorem>"))))
+
+    (alerts
+      ((cargo-deny-red . "check workspace license vs deny.toml allow-list; precedent issue #82, fix #101")
+       (governance-licence-consistency-red . "infrastructure baseline-red on main per #59 — non-blocking")
+       (scorecard-startup-failure . "PARKED per feedback_scorecard_startup_failure_2026_06_02_park; do not re-attempt the three surface fixes")
+       (proof-axiom-slippage . "Print Assumptions guard fails — investigate before merge")
+       (drift-threshold-exceeded . "drift_monitor coordinates self-normalisation; check verisim-drift logs")))
+
+    (contacts
+      ((maintainer . "Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>")
+       (estate-policy . ".claude/CLAUDE.md + ~/.claude/projects/.../memory/")
+       (hypatia-pipeline . "hypatia/lib/verisim_connector.ex + hypatia#416")
+       (panic-attack-pipeline . "panic-attack/src/* + panic-attack#101")))))

.machine_readable/6a2/README.adoc

@@ -0,0 +1,20 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+# A2ML 6a2 Directory
+
+This directory contains the 6 core A2ML machine-readable metadata files for this repository.
+
+## Files
+
+- `AGENTIC.a2ml` - AI agent operational gating, safety controls
+- `ECOSYSTEM.a2ml` - Project ecosystem position, relationships, explicit boundaries
+- `META.a2ml` - Architecture decisions (ADRs), development practices, design rationale
+- `NEUROSYM.a2ml` - Symbolic semantics, composition algebra
+- `PLAYBOOK.a2ml` - Executable plans, operational runbooks
+- `STATE.a2ml` - Project state, phase, milestones, session history
+
+## Standards Compliance
+
+These files follow the A2ML Format Family specification from:
+https://github.com/hyperpolymath/standards/tree/main/a2ml
+