docs: resolve verified .md to .adoc structural drift (#242)

.claude/CLAUDE.md

@@ -12,7 +12,7 @@ The following files in `.machine_readable/` contain structured project metadata:
 
 ## Canonical Roadmap
 
-See [`docs/ROADMAP.md`](../docs/ROADMAP.md) for the single source of truth on
+See [`docs/ROADMAP.adoc`](../docs/ROADMAP.adoc) for the single source of truth on
 where ECHIDNA is going: the 8‑stage map, row‑by‑row endpoint targets,
 current sprint (S1–S5), and agent‑tier guidance.  Record decisions
 there, not in chat.

.github/PROVEN-INTEGRATION.md

@@ -12,7 +12,7 @@ This document outlines the recommended [proven](https://github.com/hyperpolymath
 
 ## Integration Notes
 
-ECHIDNA as a neurosymbolic theorem proving platform (12 core backends exposed by default; see [docs/PROVER_COUNT.md](../docs/PROVER_COUNT.md) for the full tier table and count semantics) requires formally verified proof management:
+ECHIDNA as a neurosymbolic theorem proving platform (12 core backends exposed by default; see [docs/PROVER_COUNT.adoc](../docs/PROVER_COUNT.adoc) for the full tier table and count semantics) requires formally verified proof management:
 
 - **SafeGraph** models proof dependencies as DAGs. The `Acyclic` proof guarantees no circular dependencies in proof chains, and `topoSort` provides correct ordering for proof verification. `PathExists` verifies lemma reachability.
 

.github/canonical-references/prover-counts.yml

@@ -2,7 +2,7 @@
 # SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 #
 # R5 canonical-reference rule: bare prover counts in load-bearing
-# top-level docs must defer to docs/PROVER_COUNT.md (the canonical
+# top-level docs must defer to docs/PROVER_COUNT.adoc (the canonical
 # tier table).
 #
 # Consumed by the `Canonical-reference drift (R5 generic)` step in
@@ -17,7 +17,7 @@ id: prover-counts
 description: |
   Bare prover counts (variants vs impl files vs advertised vs core)
   in narrative-carrying top-level docs must defer to
-  docs/PROVER_COUNT.md so they cannot drift. Patterns are anchored
+  docs/PROVER_COUNT.adoc so they cannot drift. Patterns are anchored
   with (^|[[:space:]]) so neighbours like Tier-1, v1.2.3, port 8081
   don't false-positive.
 
@@ -30,7 +30,7 @@ patterns:
   - '(^|[[:space:]])[0-9]+[[:space:]]+backend[[:space:]]+implementation[[:space:]]+files?\b'
   - '(^|[[:space:]])[0-9]+/[0-9]+[[:space:]]+(backends?|provers?)\b'
 
-canonical_pointer: docs/PROVER_COUNT.md
+canonical_pointer: docs/PROVER_COUNT.adoc
 
 scope:
   include:
@@ -46,5 +46,5 @@ scope:
     - RSR_COMPLIANCE.adoc
     - SECURITY.md
     - MAINTAINERS.adoc
-    - AUTHORS.md
-    - CODE_OF_CONDUCT.md
+    - AUTHORS.adoc
+    - CODE_OF_CONDUCT.adoc

.github/workflows/formal-verification.yml

@@ -17,7 +17,7 @@
 #                    If Why3 availability changes, re-evaluate whether to keep
 #                    this as a required check or move to a scheduled/manual job.
 #
-# See crates/echidna-core-spark/CREUSOT-SETUP.md for local setup.
+# See crates/echidna-core-spark/CREUSOT-SETUP.adoc for local setup.
 
 name: Formal Verification (Stage 8c)
 

.gitlab/merge_request_templates/default.md

@@ -58,7 +58,7 @@ Related to #
 - [ ] Self-review of code performed
 - [ ] Comments added for complex logic
 - [ ] Documentation updated (if needed)
-- [ ] CHANGELOG.md updated (if needed)
+- [ ] CHANGELOG.adoc updated (if needed)
 - [ ] No new warnings introduced
 - [ ] SPDX headers added to new files
 - [ ] Follows RSR/CCCP compliance guidelines

.hypatia-ignore

@@ -3,7 +3,7 @@
 # Each line: <rule>:<path>
 #
 # Per CLAUDE.md: 'migrate existing src/rescript/ to AffineScript per
-# docs/ROADMAP.md'. These exemptions hold the line while the migration
+# docs/ROADMAP.adoc'. These exemptions hold the line while the migration
 # is in progress — each entry gets removed as the matching .res file
 # is migrated to AffineScript or deleted.
 #

.machine_readable/ER.a2ml

@@ -42,7 +42,7 @@ scope   = "src/rust/core.rs + src/rust/verification/* + src/rust/dispatch.rs"
 
 # ─── 1. Term ──────────────────────────────────────────────────────────────────
 # Universal mathematical term representation shared across every prover backend
-# (see docs/PROVER_COUNT.md for the canonical count and its semantics).
+# (see docs/PROVER_COUNT.adoc for the canonical count and its semantics).
 # An ADT with 15 variants; self-referential via boxed children.
 #
 # No explicit integer PK — terms are compared structurally (PartialEq) or

.machine_readable/ROADMAP.a2ml

@@ -15,7 +15,7 @@ next-review = "2026-07-13"
 [vision]
 summary = """
 Echidna evolves from a proof-solving library (multi-backend prover surface —
-see docs/PROVER_COUNT.md — plus neurosymbolic guidance)
+see docs/PROVER_COUNT.adoc — plus neurosymbolic guidance)
 into a distributed, trustworthy proof-as-a-service platform accessible to the
 entire hyperpolymath estate and beyond.
 

.machine_readable/contractiles/adjust/Adjustfile.a2ml

@@ -105,8 +105,8 @@ Apply (where deterministic) with: just adjust-apply
 - defer-if: aide/utoipa not yet adopted; file follow-up to wire
 
 ### A023-verisim-er-schema-drift
-- description: crates/echidna-wire/schemas/verisim_er.capnp diverged from docs/architecture/VERISIM-ER-SCHEMA.md crosswalk table
-- probe: diff <(grep -E '^\| .+ \| .+ \|' docs/architecture/VERISIM-ER-SCHEMA.md) <(parse schema → rows)
+- description: crates/echidna-wire/schemas/verisim_er.capnp diverged from docs/architecture/VERISIM-ER-SCHEMA.adoc crosswalk table
+- probe: diff <(grep -E '^\| .+ \| .+ \|' docs/architecture/VERISIM-ER-SCHEMA.adoc) <(parse schema → rows)
 - severity: high
 - adjust: update whichever lags; both must move together
 - defer-if: VerisimDB upstream schema is itself in flux (federation pending)
@@ -124,7 +124,7 @@ Apply (where deterministic) with: just adjust-apply
 - description: a new prover backend is wanted (ProverKind::all_core gap)
 - probe: manual — owner identifies
 - severity: medium
-- adjust: add variant to ProverKind enum; implement ProverBackend trait; wire ProverFactory::create; tier-assign in docs/PROVER_COUNT.md
+- adjust: add variant to ProverKind enum; implement ProverBackend trait; wire ProverFactory::create; tier-assign in docs/PROVER_COUNT.adoc
 - defer-if: prover lacks open-source binary distribution
 
 ## Workflow-Adjust

.machine_readable/contractiles/bust/Bustfile.a2ml

@@ -132,7 +132,7 @@ toolchains.
 - description: `just corpus-ingest-saturation <name>` errors `Unknown corpus adapter`
 - probe: ! just corpus-ingest-saturation isabelle external_corpora/isabelle/ 2>&1 | grep -q 'Unknown'
 - severity: medium
-- recovery: confirm dispatcher in src/rust/main.rs has match arm for <name>; if not, file PR (see docs/training-runs/2026-06-02.md follow-ups)
+- recovery: confirm dispatcher in src/rust/main.rs has match arm for <name>; if not, file PR (see docs/training-runs/2026-06-02.adoc follow-ups)
 - escalation: until dispatcher fix lands, fall back to the 4 supported adapters (agda/coq/lean/idris2)
 
 ### B052-bson-undefined-at-save

.machine_readable/contractiles/intend/Intentfile.a2ml

@@ -10,7 +10,7 @@ Declared intent and purpose for Echidna.
 
 Echidna is a trust-hardened neurosymbolic theorem proving platform.
 It supports 141 ProverKind variants over 105 backend implementations
-(canonical count semantics: docs/PROVER_COUNT.md), records every proof attempt to
+(canonical count semantics: docs/PROVER_COUNT.adoc), records every proof attempt to
 VeriSimDB, and feeds the Hypatia learning loop so the fleet gets
 smarter over time.
 
@@ -19,7 +19,7 @@ adapters for Agda, Coq, Lean 4, and Idris 2; emits 8-modality
 declaration octads compatible with VeriSim's `/api/v1/octads`; and
 runs simulated-annealing design-search + 007-style swarm dispatchers
 over candidate axiomatisations and rank functions. See
-`docs/CORPUS.md` and `docs/decisions/2026-04-28-corpus-and-design-
+`docs/CORPUS.adoc` and `docs/decisions/2026-04-28-corpus-and-design-
 search.md`.
 
 ## Anti-Purpose

.machine_readable/contractiles/trust/Trustfile.a2ml

@@ -117,7 +117,7 @@ file PRs against non-main branches.
 - description: dispatch.rs invokes mutation testing
 - run: grep -q 'MutationTester\|mutation::run' src/rust/dispatch.rs
 - severity: medium
-- recovery: re-wire per docs/handover/STATE.md trust-pipeline section
+- recovery: re-wire per docs/handover/STATE.adoc trust-pipeline section
 
 ### T033-pareto-frontier-tracked
 - description: dispatch results pass through Pareto frontier ranking
@@ -143,7 +143,7 @@ file PRs against non-main branches.
 - description: src/rust/integrity uses BLAKE3 + SHAKE3-512 for prover binary verification
 - run: grep -qE 'blake3::|shake3|Shake3_512' src/rust/integrity/*.rs
 - severity: high
-- recovery: re-add per docs/ARCHITECTURE.md integrity section
+- recovery: re-add per docs/ARCHITECTURE.adoc integrity section
 
 ## ABI-Trust
 

.machine_readable/deployment.a2ml

@@ -2,13 +2,13 @@
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # deployment.a2ml — public hosting topology for ECHIDNA.
-# Human-facing companion: docs/HOSTING.md (keep the two in step).
+# Human-facing companion: docs/HOSTING.adoc (keep the two in step).
 
 [metadata]
 version = "1.0.0"
 last-updated = "2026-07-29"
 maintainer = "Jonathan D.A. Jewell (hyperpolymath)"
-companion-doc = "docs/HOSTING.md"
+companion-doc = "docs/HOSTING.adoc"
 
 [dns]
 zone = "nesy-prover.dev"
@@ -46,7 +46,7 @@ image-published-by = ".github/workflows/ghcr-publish.yml"
 image-public = true
 deploy-unit = "deploy/hetzner/"
 runbook = "deploy/hetzner/README.adoc"
-canonical-api-doc = "site/docs/api/core.md"
+canonical-api-doc = "site/docs/api/core.adoc"
 status = "ready-not-deployed"
 
 [surfaces.api.limits]

.machine_readable/descriptiles/AGENTIC.a2ml

@@ -4,7 +4,7 @@
 # AGENTIC.a2ml — AI agent operational gating and proof-solving dispatch
 # Defines safety constraints, entropy budgets, and explicit-intent gating for AI agents
 # working in echidna (proof-solving service; 141 ProverKind variants over 105 backend
-# implementations — see docs/PROVER_COUNT.md for count semantics; 3GB training corpus).
+# implementations — see docs/PROVER_COUNT.adoc for count semantics; 3GB training corpus).
 
 [metadata]
 version = "0.3.0"

.machine_readable/descriptiles/ECOSYSTEM.a2ml

@@ -15,7 +15,7 @@ full-name = "Extensible Cognitive Hybrid Intelligence for Deductive Neural Assis
 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.md. Sandboxed solver
+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."""
 role = "prover-dispatcher"
@@ -47,7 +47,7 @@ cold-start-note = "Isabelle Main heap ~1-2GB maps at first use; Julia JIT runs o
 
 # ─────────────────────────────────────────────────────────────────────────────
 # Saturation campaign 2026-06-01 — external corpus / vocab / exchange sources
-# Branch: prover-corpus-saturation. ADR: docs/decisions/2026-06-01-saturation-campaign.md
+# Branch: prover-corpus-saturation. ADR: docs/decisions/2026-06-01-saturation-campaign.adoc
 # ─────────────────────────────────────────────────────────────────────────────
 
 [corpus-sources]

.machine_readable/descriptiles/META.a2ml

@@ -19,8 +19,8 @@ phase = "v2.2.0 — N-dim corpus + design-search + swarm landed"
 notes = """
 2026-04-28: corpus subsystem expanded into an N-dimensional / 8-
 modality / cross-prover index, with simulated-annealing design-search
-and 007 swarm dispatcher driving it. See docs/CORPUS.md and
-docs/decisions/2026-04-28-corpus-and-design-search.md.
+and 007 swarm dispatcher driving it. See docs/CORPUS.adoc and
+docs/decisions/2026-04-28-corpus-and-design-search.adoc.
 """
 
 [dependencies]
@@ -34,7 +34,7 @@ rest = 8000
 
 # ─────────────────────────────────────────────────────────────────────────────
 # Saturation campaign 2026-06-01 — additive surface declaration
-# Branch: prover-corpus-saturation. ADR: docs/decisions/2026-06-01-saturation-campaign.md
+# Branch: prover-corpus-saturation. ADR: docs/decisions/2026-06-01-saturation-campaign.adoc
 # ─────────────────────────────────────────────────────────────────────────────
 
 [saturation-campaign]
@@ -86,10 +86,10 @@ synonyms = [
 
 [saturation-campaign.new-docs]
 docs = [
-  "docs/architecture/VERISIM-ER-SCHEMA.md",
-  "docs/CORPUS-ADAPTERS.md",
-  "docs/decisions/2026-06-01-saturation-campaign.md",
-  "docs/handover/PROVER-CORPUS-SATURATION-LANE.md",
+  "docs/architecture/VERISIM-ER-SCHEMA.adoc",
+  "docs/CORPUS-ADAPTERS.adoc",
+  "docs/decisions/2026-06-01-saturation-campaign.adoc",
+  "docs/handover/PROVER-CORPUS-SATURATION-LANE.adoc",
 ]
 
 [saturation-campaign.new-schemas]

.machine_readable/descriptiles/NEUROSYM.a2ml

@@ -245,7 +245,7 @@ banned-patterns = ["believe-me", "unsafeCoerce", "Admitted", "sorry"]
 neurosym-rules-file = "standards-repo/neurosym-a2ml/hypatia-ruleset.json"
 
 # === SATURATION CAMPAIGN 2026-06-01 — arbitration + cross-prover index ===
-# Branch: prover-corpus-saturation. ADR: docs/decisions/2026-06-01-saturation-campaign.md
+# Branch: prover-corpus-saturation. ADR: docs/decisions/2026-06-01-saturation-campaign.adoc
 # Additive — preserves all existing operation-definitions / type-system / hypatia-config keys.
 
 [arbitration-extension]

.machine_readable/descriptiles/STATE.a2ml

@@ -1020,7 +1020,7 @@ here so the work has clear targets when picked up.
 """
 
 [migration-roadmap.affinescript-to-affinescript]
-status = "in-progress (per docs/ROADMAP.md), 30 files outstanding"
+status = "in-progress (per docs/ROADMAP.adoc), 30 files outstanding"
 inventory = """
 echidna/src/affinescript/ — 30 .res files split between:
   src/affinescript/src/                 — 10 production files (Main, Server,
@@ -1031,7 +1031,7 @@ echidna/src/affinescript/ — 30 .res files split between:
   src/affinescript/lib/ocaml/           — 10 generated/compiled mirrors
   + 10 ancillary
 """
-target = "AffineScript-TEA per docs/ROADMAP.md (compiled to typed-wasm, served via Deno)"
+target = "AffineScript-TEA per docs/ROADMAP.adoc (compiled to typed-wasm, served via Deno)"
 prereqs = """
 - AffineScript compiler stable enough to handle React-equivalent component
   primitives (rsr-template-repo/affinescript/ has working examples but the
@@ -1120,7 +1120,7 @@ echidna-graphql binary now builds clean. Changes:
 panic-attack assail: 4 weak points (ffi_wrapper.rs UnsafeCode — expected FFI boundary; covered by assail-classifications.a2ml)
 """
 f4-result = "panic-attack test suite was already 200/0 pass (db603c3 fixed schema_version + safe_unwrap_calls fixtures). No changes needed."
-f6-result = "audits/audit-ffi-boundary.md (4-section safety audit) + audits/assail-classifications.a2ml (7 classifications: ffi/mod.rs ×2, spark_axiom.rs, proof_search.rs, graphql/grpc/rest ffi_wrapper.rs) committed at b4d682b."
+f6-result = "audits/audit-ffi-boundary.adoc (4-section safety audit) + audits/assail-classifications.a2ml (7 classifications: ffi/mod.rs ×2, spark_axiom.rs, proof_search.rs, graphql/grpc/rest ffi_wrapper.rs) committed at b4d682b."
 workspace-build = "cargo build -p echidna -p echidna-graphql -p echidna-grpc -p echidna-rest: Finished clean (warnings only). echidna-wire fails on capnp system binary missing — pre-existing, not caused by this batch."
 metadata.last-updated = "2026-04-26"
 
@@ -1133,7 +1133,7 @@ run-url = "UNKNOWN — inspect manually: https://github.com/hyperpolymath/echidn
 jobs-green = "UNKNOWN"
 jobs-red = "UNKNOWN"
 wave-1-status = "UNKNOWN — run data inaccessible; Wave-1 is every-PR so also runs on push to main"
-wave-2-status = "UNKNOWN — run data inaccessible; CI-unverified per P0 row in docs/handover/TODO.md"
+wave-2-status = "UNKNOWN — run data inaccessible; CI-unverified per P0 row in docs/handover/TODO.adoc"
 issues-opened = []
 triage-result = "BLOCKED"
 blockers = [
@@ -1267,8 +1267,8 @@ remaining-open = [
   "GNN embeddings via Julia /gnn/embed (deferred ML training column)",
 ]
 new-docs = [
-  "docs/CORPUS.md — user-facing guide for the corpus subsystem",
-  "docs/decisions/2026-04-28-corpus-and-design-search.md — ADR record",
+  "docs/CORPUS.adoc — user-facing guide for the corpus subsystem",
+  "docs/decisions/2026-04-28-corpus-and-design-search.adoc — ADR record",
 ]
 
 [session-2026-04-28-eod-update]
@@ -1325,7 +1325,7 @@ not-done = [
 ]
 
 [session-2026-05-19-ci-baseline-triage]
-summary = "Landed PR #73 (Wave-3 consolidation, MERGED d3db97d) + triaged its red CI into 3 classes (real PR defect / baseline-rot / #77 infra jam) + cleared the two baseline blockers as dedicated PRs. Human ADR: docs/decisions/2026-05-19-ci-baseline-triage.md."
+summary = "Landed PR #73 (Wave-3 consolidation, MERGED d3db97d) + triaged its red CI into 3 classes (real PR defect / baseline-rot / #77 infra jam) + cleared the two baseline blockers as dedicated PRs. Human ADR: docs/decisions/2026-05-19-ci-baseline-triage.adoc."
 required-merge-gate = ["Analyze (rust)", "Cargo check + clippy + fmt", "Dependency audit", "Dogfood Gate", "Hypatia Neurosymbolic Analysis", "OpenSSF Scorecard"]
 findings = [
   "Triage rule: a red echidna PR check is one of (1) real in-scope PR defect, (2) baseline-rot — fails identically on origin/main, fix in dedicated PR not on the feature branch, (3) #77 infra jam — runner unassigned or ~15-30s fast-fail with EMPTY --log-failed. Verify class via `git show origin/main:<path>` + check main's run before patching.",
@@ -1338,7 +1338,7 @@ changes = [
   "PR #73 (MERGED d3db97d 17:49Z): added `COPY crates ./crates` + `COPY benches ./benches` to .containerization/Containerfile + Containerfile.full (were stale vs the crates/* workspace; wave3 + mcp were already correct).",
   "Issue #85 -> PR #86 (fix/rust-ci-drop-all-features): rust-ci.yml clippy/doc/check KEEP --all-features (no link, full coverage); the 2 cargo-test steps -> --features verisim (sole pure-Rust optional feat; live-provers superset). Avoids blinding ~510 LoC flint + spark-FFI to CI. Validated: Test Suite X(main)->ok(#86) 3m18s; local cargo test --lib --features verisim = 1092 pass/0 fail.",
   "PR #87 (fix/clusterfuzzlite-dockerfile-symlink): tracked symlink .clusterfuzzlite/Dockerfile -> Containerfile (git mode 120000); clusterfuzzlite action hardcodes Dockerfile, keeps house Containerfile name, zero blast radius. Non-gating hygiene.",
-  "docs/decisions/2026-05-19-ci-baseline-triage.md — human-readable ADR of the above (companion to this block).",
+  "docs/decisions/2026-05-19-ci-baseline-triage.adoc — human-readable ADR of the above (companion to this block).",
 ]
 not-done = [
   "#86 + #87 BLOCKED solely on #77 (required jobs awaiting runner assignment); auto-merge-squash armed, will self-fire when #77 clears. Do NOT admin-override.",
@@ -1385,15 +1385,15 @@ exchange_bridges_list = [
 ]
 
 er_schema_status = "formalised"
-er_schema_doc_path = "docs/architecture/VERISIM-ER-SCHEMA.md"
+er_schema_doc_path = "docs/architecture/VERISIM-ER-SCHEMA.adoc"
 er_schema_capnp_path = "crates/echidna-wire/schemas/verisim_er.capnp"
 
 [saturation-campaign]
 date = "2026-06-01"
 branch = "prover-corpus-saturation"
 status = "complete"
-adr = "docs/decisions/2026-06-01-saturation-campaign.md"
-handover = "docs/handover/PROVER-CORPUS-SATURATION-LANE.md"
+adr = "docs/decisions/2026-06-01-saturation-campaign.adoc"
+handover = "docs/handover/PROVER-CORPUS-SATURATION-LANE.adoc"
 commits = [
   "f73ee00", "46a7408", "6019860", "3828056", "d05dfff",
   "4a0b068", "c61140c", "85c1b8c", "cb8caff",

.trusted-base-ignore

@@ -18,7 +18,7 @@
 # substring grep cannot distinguish "uses the pattern" from "names the
 # pattern in a detector table", so every entry shows up as a false
 # positive. Same FP class as the `\bbelieve_me\b` Idris2 audit recorded
-# in docs/PROOF-NEEDS.md §"believe_me audit (2026-05-18)".
+# in docs/PROOF-NEEDS.adoc §"believe_me audit (2026-05-18)".
 #
 # These files are the *implementation* of the trust-pipeline's
 # axiom-tracker — they're proof infrastructure, not proof escapes.