ARCHITECTURE.adoc

ECHIDNA Architecture

Status: canonical human-readable overview. Lives alongside the machine-readable .machine_readable/descriptiles/META.a2ml (architecture decisions) and STATE.a2ml (current state). Last revised: 2026-11-04.

ECHIDNA — Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance — is the reasoning substrate of the hyperpolymath ecosystem. Two non-negotiable invariants govern every design choice:

1. ML suggests; provers verify. Neural components rank, route, and propose; formal provers carry the trust. A wrong suggestion is a wasted CPU cycle, not a wrong proof.

2. Trust depends on the checker and execution path. The in-tree Alethe checker validates step structure, not logical correctness. The DRAT/LRAT helper invokes drat-trim when called; that is a separate capability, not a guarantee that every proof path uses it. The echidna prove CLI calls the selected backend directly and does not independently check a certificate. This overview therefore makes no blanket claim of independent Alethe or TSTP proof reproduction. Solver identity is not checked today: the integrity step exists, nothing in the tree attaches a checker, so binaries are currently assumed rather than verified. See the Integrity caveat below and DEBT D9. Do not read this list as a guarantee that the binary you invoked is the binary you pinned.

Component map

┌─────────────────────────────────────────────────────────────────────────┐
│                              UI Layer                                   │
│   TEA sources: src/ui/tea/; static shell: src/ui/public/      │
└──────────────────────────────┬──────────────────────────────────────────┘
                               │ HTTP / WebSocket (Cap'n Proto, planned L1)
┌──────────────────────────────▼──────────────────────────────────────────┐
│                       Rust Core  (src/rust/, crates/)                   │
│                                                                         │
│  ┌──────────┐  ┌──────────────┐  ┌────────────────┐  ┌──────────────┐  │
│  │ CLI/REPL │  │ REST          │  │ gRPC          │  │ FFI (Zig)    │  │
│  │ (main.rs)│  │ (axum :8000)  │  │ (tonic :50051)│  │ (16 exports) │  │
│  └────┬─────┘  └──────┬────────┘  └──────┬────────┘  └──────┬───────┘  │
│       └────────────────┴──────────────────┴────────────────┘            │
│                                  │                                       │
│                                  ▼                                       │
│              ┌──────────────────────────────────────┐                   │
│              │  ProverDispatcher (dispatch.rs)       │                   │
│              │  — selects backend, owns trust loop   │                   │
│              └──┬───────────────────────────────┬───┘                   │
│                 │                               │                        │
│   ┌─────────────▼────────────┐    ┌─────────────▼───────────────────┐   │
│   │   Trust pipeline          │    │  141 ProverKind variants         │  │
│   │   (verification/)         │    │  105 backend impl files          │  │
│   │   - integrity             │    │  (provers/)                      │  │
│   │   - portfolio             │    │  see docs/PROVER_COUNT.adoc      │  │
│   │   - certificates          │    │                                  │  │
│   │   - axiom tracker         │    │                                  │  │
│   │   - confidence            │    │  Tier 1: 12 core (REST default)  │  │
│   │   - mutation              │    │  Tier 2–10: by capability        │  │
│   │   - pareto                │    └──────────────────────────────────┘  │
│   │   - statistics            │                                          │
│   └───────────────────────────┘                                          │
│                                                                         │
│   ┌────────────────────────┐    ┌────────────────────────┐              │
│   │ Agentic search          │    │ GNN client              │             │
│   │ (agent/, actor model)   │───►│ (gnn/client.rs)         │             │
│   └────────────────────────┘    └─────────┬──────────────┘              │
└─────────────────────────────────────────────┼────────────────────────────┘
                                              │ POST /gnn/rank
                                              │ POST /training/update
                                              │ POST /gnn/health
                  ┌───────────────────────────▼───────────────────────────┐
                  │  Julia ML sidecar  (src/julia/)  — port 8090          │
                  │   api/server.jl (canonical entry)                     │
                  │   - load_gnn_model → models/neural/gnn_ranker         │
                  │   - PROVER_DOMAIN_WEIGHTS (online from /training/update)│
                  │   - cosine fallback (model_loaded == false)           │
                  └───────────────────────┬───────────────────────────────┘
                                          │
                                          ▼
                                     VeriSimDB
                          (cross-repo; verisim REST :8080)
                          historical proof_attempts table,
                          mv_prover_success_by_class

Tier overview

ECHIDNA carries 141 ProverKind variants across 105 backend implementation files. The exposed surface depends on tier:

• Tier 1 (12 core) — the default REST /api/verify surface, and exactly the set returned by ProverKind::all_core(): Coq, Lean 4, Agda, Isabelle/HOL, Z3, CVC5, Metamath, HOL Light, Mizar, PVS, ACL2, HOL4.

• Tier 2–10 — the remaining variants: ATPs, SMT, model checkers, constraint solvers, niche provers, ecosystem type-checkers. Available via explicit ProverKind selection in CLI / REPL / GraphQL but not auto-routed.

See PROVER_COUNT.adoc for the canonical tier table and per-prover capabilities.

Trust pipeline walkthrough

Each verify_proof call passes through (under --features verisim, eventually in default builds; see handover/TODO.adoc for current state):

1. Integrity (integrity/) — solver binary SHAKE3-512 + BLAKE3 against config/solver-manifest.toml. Caveat, 2026-11-01: this step runs only when a checker is attached, and nothing in the tree calls with_integrity_checker; unconfigured, the pipeline treats integrity as passing (dispatch.rs:632). The manifest also still holds PLACEHOLDER_COMPUTE_ON_FIRST_RUN for every solver. Treat this step as not executed until it is wired; see docs/reports/2026-11-01-routing-and-rule-engine-recon.adoc §6 RD5.

2. Dispatch (dispatch.rs) — ProverDispatcher::select_prover picks the backend; under with_verisim, VeriSimAdvisor queries mv_prover_success_by_class for historical success-rate hints.

3. Sandbox (executor/) — Podman or bubblewrap process containment.

4. Portfolio cross-check (verification/portfolio.rs) — for SMT, run two independent solvers; ✓ if both agree.

5. Certificate verification (verification/certificates.rs) — replay Alethe / DRAT-LRAT / TSTP independently of the originating solver.

6. Axiom tracking (verification/axiom_tracker.rs) — 4 danger levels (Safe, Noted, Warning, Reject).

7. Confidence (verification/confidence.rs) — 5-tier Bayesian trust score.

8. Mutation testing (verification/mutation.rs) — for specifications.

9. Pareto (verification/pareto.rs) — multi-objective frontier across speed / trust / certificate availability.

10. Statistics (verification/statistics.rs) — per-(prover, domain) success rates; exported to /training/update for online ML weight updates.

11. Outcome emission (dispatch.rs::spawn_record_attempt, gated on with_verisim_writer) — fire-and-forget write to VeriSimDB proof_attempts, closes the learning loop.

Client-facing surfaces, and what VeriSimDB is not

There are four independent listeners, not one service on four ports. Each is a separate binary with its own route table and its own path to the provers:

Listener	Default bind	Route root
echidna server	127.0.0.1:8081	/api/* — /api/health, /api/provers, /api/prove, /api/verify, /api/session/*, …
echidna-rest	127.0.0.1:8000	/api/v1/* plus root /health
echidna-graphql	127.0.0.1:8082	POST / (GraphQL), GET / (playground), /health
echidna-grpc	[::1]:50051	ProofService over echidna.proto

echidna-graphql moved from 8081 to 8082 on 2026-11-04 so it can run alongside the core server. ECHIDNA_GRAPHQL_ADDR remains an override; deployments deliberately retaining the old GraphQL address must set it explicitly and avoid binding the core server there.

VeriSimDB is a persistence and learning adapter, not a communication path. It sits behind the non-default verisim Cargo feature, is written to fire-and-forget after a dispatch, and is never consulted to reach a prover. Clients do not route through it, and must not need to: the estate’s 3-practice/PROOF-POLICY.adoc §2.2 states that ECHIDNA is “the longer-term automation destination, not a prerequisite for current independent checks”. A mandatory VCL hop would violate that. Two consequences worth knowing before you deploy:

• Enabling verisim also moves POST /api/prove onto ProverDispatcher (server.rs:423); without it, /api/prove goes to the backend factory directly. A storage feature should not decide the verification route.

• /api/verify never enters the dispatcher at all, and /api/verify_raw executes the solver binary directly by design.

So "which pipeline ran" depends on the surface and the feature set. If a client needs a machine-readable answer it can trust, use echidna prove <file> --output json — the documented echidna.prove.result/1 contract — rather than inferring it from an HTTP response body.

Polyglot source layout

src/ holds one subdirectory per language. The split is intentional — see RSR_COMPLIANCE.adoc §“Out-of-template adaptations”.

Path	Language	Role
src/rust/	Rust	Core: backends, dispatch, trust pipeline, CLI, REPL, server
crates/	Rust	Extracted workspace members (echidna-core, -mcp, -wire, -core-spark, typed_wasm)
src/julia/	Julia	ML sidecar (GNN, logistic regression, training, eval)
src/abi/	Idris 2	Formal ABI proofs (16 modules, zero believe_me)
src/idris/	Idris 2	UI validator
src/chapel/	Chapel	Parallel proof search (L2.1 live; L2.2+ gated)
src/zig_ffi/	Zig	Chapel-bridge FFI shim
ffi/zig/	Zig	Overlay / tentacles / boj sources
src/ada/	Ada + SPARK	Formal companion library
src/ui/tea/	AffineScript-TEA	UI sources (compile pipeline unavailable)
src/ui/public/	HTML/static assets	Browser shell; open prove.html directly
src/interfaces/	Rust	GraphQL, gRPC, REST workspace crates

Internal IPC

Today: HTTP + JSON between Rust core and Julia sidecar on port 8090. Endpoints — POST /gnn/rank, POST /gnn/embed, POST /training/update, POST /gnn/health, plus POST /reload (planned port from the orphaned api_server.jl).

Planned (Stage 5a / L1): Cap’n Proto over Unix domain socket; HTTP+JSON retained only as debug fallback. See docs/handover/L1-CAPNPROTO-PROMPT.adoc.

Where to go next

• docs/ROADMAP.adoc — canonical stage map and sprint targets.

• docs/handover/STATE.adoc — running session log.

• docs/handover/HANDOVER-INDEX.adoc — guide to the handover/ prompt suite.

• docs/ENV-VARS.adoc — every environment variable the system reads, with defaults.

• docs/PROVER_COUNT.adoc — canonical tier table.

• .machine_readable/descriptiles/STATE.a2ml — machine-readable state, regenerated each sprint.