docs: repo-wide documentation refresh — counts, paths, licence status, debt register

.claude/CLAUDE.md

@@ -2,12 +2,12 @@
 
 The following files in `.machine_readable/` contain structured project metadata:
 
-- `.machine_readable/6a2/STATE.a2ml` - Current project state and progress
-- `.machine_readable/6a2/META.a2ml` - Architecture decisions and development practices
-- `.machine_readable/6a2/ECOSYSTEM.a2ml` - Position in the ecosystem and related projects
-- `.machine_readable/6a2/AGENTIC.a2ml` - AI agent interaction patterns
-- `.machine_readable/6a2/NEUROSYM.a2ml` - Neurosymbolic integration config
-- `.machine_readable/6a2/PLAYBOOK.a2ml` - Operational runbook
+- `.machine_readable/descriptiles/STATE.a2ml` - Current project state and progress
+- `.machine_readable/descriptiles/META.a2ml` - Architecture decisions and development practices
+- `.machine_readable/descriptiles/ECOSYSTEM.a2ml` - Position in the ecosystem and related projects
+- `.machine_readable/descriptiles/AGENTIC.a2ml` - AI agent interaction patterns
+- `.machine_readable/descriptiles/NEUROSYM.a2ml` - Neurosymbolic integration config
+- `.machine_readable/descriptiles/PLAYBOOK.a2ml` - Operational runbook
 - `.machine_readable/bot_directives/*.a2ml` - Per-bot permission and scope rules
 
 ## Canonical Roadmap

.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 supporting 128 prover backends (12 core; see [docs/PROVER_COUNT.md](../docs/PROVER_COUNT.md)) requires formally verified proof management:
+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:
 
 - **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.
 

.machine_readable/ER.a2ml

@@ -41,8 +41,9 @@ scope   = "src/rust/core.rs + src/rust/verification/* + src/rust/dispatch.rs"
 # ═══════════════════════════════════════════════════════════════════════════════
 
 # ─── 1. Term ──────────────────────────────────────────────────────────────────
-# Universal mathematical term representation shared across all 105 prover
-# backends.  An ADT with 15 variants; self-referential via boxed children.
+# Universal mathematical term representation shared across every prover backend
+# (see docs/PROVER_COUNT.md 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
 # via Display serialisation for hashing in proof_encoding.rs.

.machine_readable/ROADMAP.a2ml

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

.machine_readable/contractiles/intend/Intentfile.a2ml

@@ -9,7 +9,8 @@ Declared intent and purpose for Echidna.
 ## Purpose
 
 Echidna is a trust-hardened neurosymbolic theorem proving platform.
-It supports 128 prover backends, records every proof attempt to
+It supports 141 ProverKind variants over 105 backend implementations
+(canonical count semantics: docs/PROVER_COUNT.md), records every proof attempt to
 VeriSimDB, and feeds the Hypatia learning loop so the fleet gets
 smarter over time.
 

.machine_readable/descriptiles/AGENTIC.a2ml

@@ -3,7 +3,8 @@
 #
 # 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 with 105 prover backends, 3GB training corpus).
+# working in echidna (proof-solving service; 141 ProverKind variants over 105 backend
+# implementations — see docs/PROVER_COUNT.md for count semantics; 3GB training corpus).
 
 [metadata]
 version = "0.3.0"

.machine_readable/descriptiles/ECOSYSTEM.a2ml

@@ -12,10 +12,12 @@ ecosystem = "hyperpolymath"
 [project]
 name = "ECHIDNA"
 full-name = "Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance"
-purpose = """Trust-hardened neurosymbolic theorem proving platform. 48 prover backends
-(Agda, Lean4, Isabelle, Coq, Idris2, F*, Z3, CVC5, Vampire, and 39 more). Sandboxed
-solver execution (Podman/bubblewrap), proof certificate checking, axiom tracking,
-GNN-guided proof search, Julia ML inference layer."""
+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
+execution (Podman/bubblewrap), proof certificate checking, axiom tracking, GNN-guided
+proof search, Julia ML inference layer."""
 role = "prover-dispatcher"
 
 [position]

0-AI-MANIFEST.a2ml

@@ -46,7 +46,7 @@ proofs = "proofs/"
 container = "container/"
 
 [tech-stack]
-primary = "Rust (48 prover backends, trust pipeline, CLI, REPL, API servers)"
+primary = "Rust (141 ProverKind variants over 105 backend implementations — see docs/PROVER_COUNT.md; trust pipeline, CLI, REPL, API servers)"
 secondary = "Julia (ML inference, port 8090), ReScript+Deno (UI, 33 files, zero TypeScript)"
 optional = "Chapel (parallel proof dispatch)"
 abi = "Idris2 (7 modules, zero believe-me)"
@@ -56,8 +56,9 @@ build = "Justfile (primary), Cargo workspace"
 container = "Podman + Containerfile"
 
 [architecture]
-# Trust-hardened neurosymbolic theorem proving with 48 prover backends
-core = "src/rust/"                  # 48 provers, trust pipeline, dispatch
+# Trust-hardened neurosymbolic theorem proving; canonical backend count and
+# count semantics live in docs/PROVER_COUNT.md
+core = "src/rust/"                  # ProverKind enum + backends, trust pipeline, dispatch
 verification = "src/rust/verification/" # Portfolio, certificates, axiom tracker, confidence, mutation, pareto, statistics
 integrity = "src/rust/integrity/"   # Solver binary integrity (SHAKE3-512, BLAKE3)
 executor = "src/rust/executor/"     # Sandboxed execution (Podman, bubblewrap)

AFFIRMATION.adoc

@@ -36,7 +36,7 @@ available.
   real release line is in `CHANGELOG.md`.
 . *Critical Reception Grade.* CRG-C is complete (unit + smoke + build + P2P +
   E2E + contract + aspect + benchmarks baselined, per
-  `.machine_readable/6a2/STATE.a2ml`); CRG-B criteria are populated but B is
+  `.machine_readable/descriptiles/STATE.a2ml`); CRG-B criteria are populated but B is
   *not* formally affirmed here.
 
 == Verified as of 2026-06-15 (green / reproduced)

ARCHITECTURE.md

@@ -1,47 +1,26 @@
-# Architecture
-
-## Overview
-
-This repository follows a modular, maintainable architecture designed for clarity, scalability, and long-term sustainability.
-
-## Directory Structure
-
-```
-.
-├── src/           # Source code
-├── tests/        # Test suites
-├── docs/         # Documentation
-├── scripts/      # Utility scripts
-├── config/       # Configuration files
-├── LICENSE       # License file
-├── LICENSES/     # Full license texts
-└── README.adoc   # Project documentation
-```
-
-## Design Principles
+<!--
+  SPDX-License-Identifier: CC-BY-SA-4.0
+  SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
-- **Separation of Concerns**: Each module has a single responsibility
-- **Testability**: Code is written to be easily testable
-- **Documentation**: All public APIs are documented
-- **Configuration**: Environment-specific settings are externalized
+  docs/ARCHITECTURE.md is canonical. This file previously held generic
+  scaffold text ("modular, maintainable architecture designed for clarity,
+  scalability...") that contained no project-specific content — it described
+  no part of ECHIDNA and duplicated nothing real. Replaced with a pointer
+  rather than deleted, because the path is referenced externally.
+-->
 
-## Dependencies
-
-- External dependencies are minimized and clearly declared
-- Version pinning is used for reproducibility
-
-## Security Considerations
-
-- Sensitive data is never committed to the repository
-- Secrets are managed through environment variables or secure vaults
-- Regular dependency audits are performed
-
-## Maintainability
+# Architecture
 
-- Code follows consistent style guidelines
-- Pull requests require review and CI checks
-- Issues and discussions are tracked transparently
+The architecture documentation for ECHIDNA lives in
+[`docs/ARCHITECTURE.md`](docs/ARCHITECTURE.md) — the polyglot layout, the
+dispatch path, the trust-hardening pipeline, and how the Rust core, Julia ML
+sidecar, Idris2 ABI, Zig FFI and optional Chapel parallel layer fit together.
 
----
+Related canonical documents:
 
-*Last updated: 2026-07-18*
+- [`docs/PROVER_COUNT.md`](docs/PROVER_COUNT.md) — backend tier table and what
+  each published count actually counts
+- [`docs/ROADMAP.md`](docs/ROADMAP.md) — stage map and current direction
+- [`docs/DEBT.md`](docs/DEBT.md) — known licence, documentation and code debt
+- [`.machine_readable/descriptiles/META.a2ml`](.machine_readable/descriptiles/META.a2ml)
+  — the machine-readable architecture record

CLAUDE.md

@@ -11,6 +11,8 @@ Guidelines and context for working with Claude Code on the ECHIDNA project.
 - **License**: AGPL-3.0-or-later (owner decision 2026-07-07; per-file MPL-2.0 headers pending migration sweep)
 - **Architecture overview**: [`docs/ARCHITECTURE.md`](docs/ARCHITECTURE.md)
 - **Canonical prover count + tier table**: [`docs/PROVER_COUNT.md`](docs/PROVER_COUNT.md)
+- **Known debt (licence, docs, code)**: [`docs/DEBT.md`](docs/DEBT.md) — read before
+  asserting anything about the licence; the repository is currently inconsistent
 - **Environment variables**: [`docs/ENV-VARS.md`](docs/ENV-VARS.md)
 - **RSR / CCCP compliance statement**: [`RSR_COMPLIANCE.adoc`](RSR_COMPLIANCE.adoc)
 - **Receipts for README claims**: [`EXPLAINME.adoc`](EXPLAINME.adoc)

CONTRIBUTING.md

@@ -15,7 +15,7 @@ and the licence / SPDX policy. GitHub renders AsciiDoc directly.
 
 If a quick orientation is enough:
 
-- **Before you start**: read [`README.adoc`](README.adoc),
+- **Before you start**: read [`README.md`](README.md),
   [`RSR_COMPLIANCE.adoc`](RSR_COMPLIANCE.adoc), and
   [`CLAUDE.md`](CLAUDE.md) (if you are using an AI agent).
 - **Local setup**: see [`QUICKSTART-DEV.adoc`](QUICKSTART-DEV.adoc).

GOVERNANCE.adoc

@@ -128,7 +128,7 @@ This repository adheres to hyperpolymath estate-wide policies:
 
 | **Contractiles** | Mustfile, Trustfile, Intendfile, Adjustfile in root
 
-| **Machine Readable** | META.a2ml in .machine_readable/6a2/
+| **Machine Readable** | META.a2ml in .machine_readable/descriptiles/
 
 | **CI/CD** | GitHub Actions workflows in .github/workflows/
 

GOVERNANCE.md

@@ -1,60 +1,24 @@
-# Governance
-
-## Overview
-
-This project is governed by the following principles and structures to ensure transparent, inclusive, and effective decision-making.
-
-## Roles and Responsibilities
-
-### Maintainers
-
-Maintainers are responsible for:
-- Reviewing and merging pull requests
-- Managing releases and versioning
-- Ensuring code quality and standards
-- Triaging issues and bug reports
-- Community engagement and support
-
-### Contributors
-
-Contributors are expected to:
-- Follow the code of conduct
-- Submit well-documented pull requests
-- Write tests for new functionality
-- Maintain existing tests
-- Update documentation as needed
+<!--
+  SPDX-License-Identifier: CC-BY-SA-4.0
+  SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
-## Decision Making
+  GOVERNANCE.adoc is canonical (RSR convention). This file previously held
+  generic scaffold text describing roles that do not correspond to this
+  project's actual governance. Replaced with a pointer rather than deleted,
+  because the path is referenced externally and GitHub's community-standards
+  check looks for it.
+-->
 
-### Minor Changes
-- Can be made by any maintainer
-- Include bug fixes, documentation updates, dependency updates
-
-### Major Changes
-- Require discussion in issues or pull requests
-- Include new features, architectural changes, API changes
-- Need approval from at least 2 maintainers
-
-### Breaking Changes
-- Require RFC (Request for Comments) process
-- Need approval from majority of maintainers
-- Must include migration guide
-
-## Code of Conduct
-
-All participants are expected to follow our Code of Conduct. Violations can be reported to the maintainers.
-
-## Communication
-
-- **Issues**: For bug reports and feature requests
-- **Discussions**: For questions and general discussion
-- **Pull Requests**: For code contributions
-
-## Licensing
+# Governance
 
-All contributions are made under the terms of the repository's LICENSE file.
-By submitting a pull request, you agree to license your contributions accordingly.
+The governance model for ECHIDNA is documented in
+[`GOVERNANCE.adoc`](GOVERNANCE.adoc) — decision-making, maintainer
+responsibilities, the RSR/CCCP compliance position, and how changes are
+ratified. GitHub renders AsciiDoc directly.
 
----
+Related:
 
-*Last updated: 2026-07-18*
+- [`MAINTAINERS.adoc`](MAINTAINERS.adoc) — who maintains what
+- [`CONTRIBUTING.adoc`](CONTRIBUTING.adoc) — contribution process
+- [`CODE_OF_CONDUCT.md`](CODE_OF_CONDUCT.md) — expected conduct
+- [`RSR_COMPLIANCE.adoc`](RSR_COMPLIANCE.adoc) — compliance statement

README.md

@@ -3,9 +3,26 @@ SPDX-License-Identifier: CC-BY-SA-4.0
 SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 
-[![OpenSSF Best Practices](https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity)](https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/echidna)
 [![License: AGPL-3.0-or-later](https://img.shields.io/badge/License-AGPL--3.0--or--later-blue.svg)](LICENSE) [![Green Hosting](https://api.thegreenwebfoundation.org/greencheckimage/nesy-prover.dev)](https://www.thegreenwebfoundation.org/green-web-check/?url=nesy-prover.dev)
 
+<!--
+The OpenSSF Best Practices badge was removed 2026-08-07: it was a hardcoded
+green shields.io label linking to the project *registration* form, so it
+displayed "passed" while the project was not registered and would have kept
+displaying it whatever the real standing. Restore the genuine dynamic badge
+once the project is registered at https://www.bestpractices.dev/ — the real
+one reports the achieved tier and changes when it lapses. Tracked as D3 in
+docs/DEBT.md.
+-->
+
+> **Licence notice.** This repository declares AGPL-3.0-or-later in `LICENSE`
+> and `Cargo.toml`, but per-file `SPDX-License-Identifier` headers across the
+> source tree still read `MPL-2.0`, and `NOTICE` still describes the project as
+> MPL-2.0. That inconsistency is unresolved — see
+> [`docs/DEBT.md`](docs/DEBT.md) (P0). If your use depends on the licence
+> terms, read `LICENSE` and ask the maintainer before relying on any other
+> surface.
+
 \*E\*xtensible \*C\*ognitive \*H\*ybrid \*I\*ntelligence for
 \*D\*eductive \*N\*eural \*A\*ssistance
 

RSR_COMPLIANCE.adoc

@@ -7,7 +7,7 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 :toc:
 
 Status: living document, regenerated as policy changes.
-Canonical state: `.machine_readable/6a2/STATE.a2ml`.
+Canonical state: `.machine_readable/descriptiles/STATE.a2ml`.
 Canonical policy: `MUST.contractile`, `ADJUST.contractile`,
 `.machine_readable/policies/*.a2ml`.
 
@@ -49,7 +49,7 @@ the contractiles and the machine-readable policies above.
 ECHIDNA diverges from the strict RSR template in three places:
 
 1. *State file location*: RSR template puts `STATE.scm` at root; echidna
-   places it at `.machine_readable/6a2/STATE.a2ml` per the `.scm → .a2ml`
+   places it at `.machine_readable/descriptiles/STATE.a2ml` per the `.scm → .a2ml`
    migration documented in `.claude/CLAUDE.md`.
 2. *Polyglot source layout*: `src/` contains per-language subdirectories
    (`src/rust/`, `src/julia/`, `src/abi/`, `src/chapel/`, `src/zig_ffi/`,

crates/echidna-mcp/README.md

@@ -50,7 +50,7 @@ Or with an explicit binary path:
 
 ### `prove`
 
-Prove a theorem from a file using one of ECHIDNA's 105 backends.
+Prove a theorem from a file using one of ECHIDNA's prover backends (see [`docs/PROVER_COUNT.md`](../../docs/PROVER_COUNT.md)).
 
 | Parameter | Type | Required | Description |
 |-----------|------|----------|-------------|

docs/ARCHITECTURE.md

@@ -4,8 +4,8 @@
 # ECHIDNA Architecture
 
 **Status**: canonical human-readable overview. Lives alongside the machine-readable
-[`.machine_readable/6a2/META.a2ml`](../.machine_readable/6a2/META.a2ml) (architecture
-decisions) and [`STATE.a2ml`](../.machine_readable/6a2/STATE.a2ml) (current state).
+[`.machine_readable/descriptiles/META.a2ml`](../.machine_readable/descriptiles/META.a2ml) (architecture
+decisions) and [`STATE.a2ml`](../.machine_readable/descriptiles/STATE.a2ml) (current state).
 Last revised: 2026-05-26.
 
 ECHIDNA — Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance —
@@ -157,4 +157,4 @@ retained only as debug fallback. See [`docs/handover/L1-CAPNPROTO-PROMPT.md`](ha
 - [`docs/ENV-VARS.md`](ENV-VARS.md) — every environment variable the system
   reads, with defaults.
 - [`docs/PROVER_COUNT.md`](PROVER_COUNT.md) — canonical tier table.
-- [`.machine_readable/6a2/STATE.a2ml`](../.machine_readable/6a2/STATE.a2ml) — machine-readable state, regenerated each sprint.
+- [`.machine_readable/descriptiles/STATE.a2ml`](../.machine_readable/descriptiles/STATE.a2ml) — machine-readable state, regenerated each sprint.

docs/CVC5_QUICK_REFERENCE.md

@@ -384,8 +384,7 @@ cvc5 problem.smt2
 
 ## Links
 
-- [Full Implementation Details](/home/user/echidna/docs/CVC5_IMPLEMENTATION.md)
-- [Implementation Summary](/home/user/echidna/CVC5_IMPLEMENTATION_SUMMARY.md)
+- [Implementation Summary](implementation/CVC5_IMPLEMENTATION_SUMMARY.md)
 - [CVC5 Documentation](https://cvc5.github.io/docs/latest/)
 - [SMT-LIB Standard](https://smtlib.cs.uiowa.edu/)