ECHIDNA

*E*xtensible *C*ognitive *H*ybrid *I*ntelligence for *D*eductive *N*eural *A*ssistance

A neurosymbolic theorem proving platform with 48 prover backends, trust-hardened verification pipeline, and multi-objective proof search.

Leadership Position

ECHIDNA holds a unique leadership position in the theorem proving ecosystem as:

• The only system with 48+ prover backends (vs 1 for Isabelle, Coq, Lean, Z3, etc.)

• The only system actively solving cross-prover arbitration (mathematical object identity resolution)

• The only neurosymbolic hybrid architecture (combining AI and symbolic reasoning)

• The only system with 7-stage trust pipeline (comprehensive verification infrastructure)

• The only system integrating OpenTheory + Dedukti (universal proof exchange)

• The largest vocabulary management (992K+ terms across mathematical domains)

• The most comprehensive axiom tracking (4 danger levels across 48 provers)

• The only Bayesian confidence scoring (across multiple independent provers)

Our prevailing advantage comes from this unique combination that no other system can match.

Overview

ECHIDNA orchestrates 48 theorem provers, SMT solvers, first-order ATPs, and constraint solvers through a unified Rust core. Every proof result passes through a trust-hardening pipeline that checks solver integrity, tracks axiom usage, verifies proof certificates, and assigns a 5-level confidence score.

Neural premise selection (via Julia) suggests tactics, but formal provers always have the final word. ECHIDNA never produces unsound proofs.

Features

48 Prover Backends

Tier	Provers
Tier 1: Interactive Proof Assistants	Agda, Coq/Rocq, Lean 4, Isabelle/HOL, Idris2, F*
Tier 2: SMT Solvers	Z3, CVC5, Alt-Ergo
Tier 3: Auto-Active Verifiers	Dafny, Why3
Tier 4: Specialised	Metamath, HOL Light, Mizar, HOL4, PVS, ACL2, TLAPS, Twelf, Nuprl, Minlog, Imandra
Tier 5: First-Order ATPs	Vampire, E Prover, SPASS
Tier 6: Constraint / Optimisation Solvers	GLPK, SCIP, MiniZinc, Chuffed, OR-Tools

All 48 backends implement the ProverBackend trait: parse, verify, export, tactic suggestion, and theorem search. File extension detection covers 30+ formats (.v, .lean, .smt2, .tptp, .dfy, .mzn, etc.).

Trust & Safety Hardening (v1.5)

The verification pipeline applies the following checks to every proof:

• Solver Binary Integrity (integrity/): SHAKE3-512 provenance hashing and BLAKE3 fast runtime re-verification. Solver binaries are checked against a TOML manifest at startup; tampered binaries are rejected.

• SMT Portfolio Solving (verification/portfolio.rs): Cross-checks proofs across multiple solvers (e.g. Z3 + CVC5 + Alt-Ergo). Flags disagreements for human review. Supports SMT, ATP, and ITP solver pools.

• Proof Certificate Checking (verification/certificates.rs): Verifies Alethe (CVC5), DRAT/LRAT (SAT solvers), TSTP (first-order ATPs), Lean4 kernel, and Coq kernel certificate formats. Certificates are hashed with BLAKE3 and stored for audit trails.

• Axiom Usage Tracking (verification/axiom_tracker.rs): Scans proof content for dangerous constructs across provers. Four danger levels:

  • Safe: Standard library axioms

  • Noted: Classical axioms in constructive systems (e.g. Axiom in Coq)

  • Warning: Incomplete proof markers (sorry, Admitted, postulate)

  • Reject: Known unsound constructs (--type-in-type, mk_thm, believe_me) Comments are not flagged.

• Solver Sandboxing (executor/sandbox.rs): Runs solvers in isolated environments. Three modes: Podman containers (preferred, --network=none, read-only, memory/CPU/disk limits), bubblewrap namespaces (fallback), or unsandboxed (development only, requires explicit opt-in). Auto-detection selects the strongest available option.

• 5-Level Trust Hierarchy (verification/confidence.rs): Every proof result receives a trust level:

  • Level 1: Large-TCB system, unchecked, or dangerous axioms used

  • Level 2: Single prover, no dangerous axioms

  • Level 3: Single prover with verified proof certificate

  • Level 4: Small-kernel prover (Lean, Coq, Isabelle, Agda, Metamath, HOL Light, HOL4, Idris2, F*, Twelf, Nuprl, Minlog) with verified certificate

  • Level 5: Cross-checked by 2+ independent small-kernel systems with certificates

• Mutation Testing (verification/mutation.rs): Deliberately weakens specifications (remove preconditions, weaken postconditions, negate subterms, replace constants) to verify the pipeline catches them. Computes a mutation score with a default 95% threshold.

• Cross-Prover Proof Exchange (exchange/): Export and import proofs in universal formats: OpenTheory (HOL family interop) and Dedukti/Lambdapi (universal proof kernel based on lambda-Pi calculus modulo rewriting).

• Pareto Optimisation (verification/pareto.rs): Multi-objective ranking of proof candidates across four axes: proof time, trust level, memory usage, and proof size. Computes the Pareto frontier and optionally applies weighted scoring for single-best selection.

• Statistical Confidence Tracking (verification/statistics.rs): Per-prover, per-domain success rates and timing statistics. Bayesian timeout estimation (mean + 2 sigma). Wilson score intervals for mutation score confidence. Prover ranking by composite score (success rate, timeout rate, speed). JSON serialisation for persistence.

• Dispatch Pipeline (dispatch.rs): Orchestrates the full pipeline: create prover → parse → verify → axiom scan → confidence scoring. Supports single-prover and cross-checked (portfolio) modes with configurable minimum trust levels.

Additional Capabilities

• Neurosymbolic ML (Julia layer): Logistic regression tactic prediction trained on 332 proofs / 1,603 tactics. Serves predictions via HTTP (port 8090).

• Aspect Tagging: Intelligent proof categorisation and domain analysis

• Anomaly Detection: ML-based overconfidence detection

• Agentic Proof Search: Actor-based autonomous proof exploration

• Chapel Parallel Layer (optional): Coforall-based parallel proof dispatch

• 3 API Interfaces:

  • GraphQL (async-graphql, port 8081)

  • gRPC (tonic + Protocol Buffers, port 50051)

  • REST (axum + OpenAPI/Swagger, port 8000)

• ReScript UI: 33 compiled components for proof exploration (zero TypeScript)

• REPL: Interactive proof session via rustyline

Quick Start

Prerequisites

• Rust nightly (managed via asdf)

• Julia 1.10+ (for ML layer)

• Deno (for ReScript UI)

• Podman (NOT Docker) — recommended for solver sandboxing

• Just command runner

Build and Test

# Clone
git clone https://github.com/hyperpolymath/echidna.git
cd echidna

# Build
just build
# or: cargo build

# Run all tests (613+ passing)
just test
# or: cargo test

# Run ECHIDNA REPL
just run

Using Podman Container

podman build -f Containerfile -t echidna:latest .
podman run -it echidna:latest

Architecture

Technology Stack

• Rust: Core logic, prover backends, trust pipeline, CLI, REPL, API servers

• Julia: ML inference (tactic prediction, premise selection)

• ReScript + Deno: UI components

• Chapel: Optional parallel proof dispatch

Key Modules

src/rust/
  provers/          # 48 prover backend implementations (ProverBackend trait)
  verification/     # Trust-hardening subsystem
    portfolio.rs    # SMT portfolio solving / cross-checking
    certificates.rs # Proof certificate checking (Alethe, DRAT/LRAT, TSTP)
    axiom_tracker.rs# Axiom usage scanning and policy enforcement
    confidence.rs   # 5-level trust hierarchy
    mutation.rs     # Mutation testing for specifications
    pareto.rs       # Pareto frontier computation
    statistics.rs   # Per-prover statistical tracking
  integrity/        # Solver binary integrity (SHAKE3-512, BLAKE3)
  executor/         # Sandboxed solver execution (Podman, bubblewrap)
  exchange/         # Cross-prover proof exchange (OpenTheory, Dedukti)
  dispatch.rs       # Full trust-hardening dispatch pipeline
  agent/            # Agentic proof search (actor model)
  neural.rs         # Neural premise selection integration
  aspect.rs         # Aspect tagging system
  anomaly_detection.rs
  proof_search.rs   # Chapel parallel proof search
  core.rs           # Core types (Term, ProofState, Tactic, Goal, etc.)
  parsers/          # Proof file parsers
  ffi/              # Foreign function interface
  server.rs         # HTTP API server
  repl.rs           # Interactive REPL
  main.rs           # CLI entry point
  lib.rs            # Library root

API Usage

use echidna::provers::{ProverFactory, ProverKind, ProverConfig};

// Create a prover backend
let backend = ProverFactory::create(ProverKind::Lean, ProverConfig::default())?;
let state = backend.parse_string("theorem foo : 1 + 1 = 2 := by omega").await?;
let verified = backend.verify_proof(&state).await?;

use echidna::dispatch::{ProverDispatcher, DispatchConfig};
use echidna::provers::ProverKind;

// Use the trust-hardening dispatch pipeline
let dispatcher = ProverDispatcher::with_config(DispatchConfig {
    cross_check: true,
    track_axioms: true,
    ..Default::default()
});

// Cross-checked verification
let result = dispatcher.verify_proof_cross_checked(
    ProverKind::Z3,
    "(set-logic QF_LIA)\n(assert (> x 0))\n(check-sat)",
    &[ProverKind::CVC5],
).await?;

println!("Verified: {}, Trust: {}", result.verified, result.trust_level);

Test Suite

613+ library tests passing (cargo test --lib, 2 ignored).

• ~528 unit tests across provers, verification, integrity, executor, agent

• 38 integration tests (with 2 pre-existing CVC5 E2E failures tracked separately)

• 21 property-based tests (PropTest)

• Additional interface and neural integration tests

cargo test              # Run all tests
cargo test --lib        # Unit tests only
cargo test --test integration_tests

Development

Quality Checks

just check      # All quality checks
just lint       # REUSE, rustfmt, clippy
just security   # Trivy, cargo-audit
just coverage   # Test coverage
just mvp        # MVP smoke checks (reports missing provers, non-fatal)

Current Status

v1.5.0 — Trust & Safety Hardening Complete

Area	Status
Prover backends	30/30 operational
Trust pipeline	All 13 tasks complete
Unit tests	232 passing
Integration tests	38 passing
Property tests	21 passing (PropTest)
API interfaces	GraphQL, gRPC, REST
ML layer	Julia logistic regression
UI	ReScript, 33 components
CI/CD	17 workflows

Completed in v2.2 (epistemic hardening):

• Typed ProverOutcome taxonomy — 8 mutually-exclusive statuses replacing Result<bool>

• Z3 check() override: inconsistency pre-check before trivial-goal short-circuit

• Z3 output parsing uses last non-empty line (not whole-output contains())

• Z3 goal-set inconsistency detection (goals cannot all hold simultaneously)

• Why3 timeout bug fixed (+5s undocumented slack removed)

• Pre-colleague sanity suite: 37 tests covering full taxonomy with Z3 integration

• /api/verify REST endpoint now returns typed outcome field alongside valid: bool

• echidnabot ProofStatus extended to full 8-variant taxonomy, backward compatible

Roadmap — v2.3 (single-session Z3):

• Replace two-process inconsistency check with single Z3 session using (push)/(pop) — atomic, halves subprocess overhead

• check_raw_smt() trait method for backends that accept pre-built content directly (bypasses lossy parse_string() round-trip)

Roadmap — v2.4 (typed override coverage):

Priority backends for typed check() overrides (currently use heuristic fallback): CVC5, Lean 4, Coq/Rocq, Isabelle. Each adds accurate INCONSISTENT_PREMISES and UNSUPPORTED_FEATURE detection for that backend.

Planned for v3.0:

• Deep learning models (Transformers via Flux.jl)

• Production deployment configuration

• Tamarin/ProVerif bridge for cipherbot

Documentation

• Contributing Guidelines

• Code of Conduct

• Security Policy

• Changelog

• Roadmap

Critical Constraints

• NO PYTHON — Julia for ML, Rust for systems, ReScript for UI

• RSR/CCCP Compliance — Rhodium Standard Repository guidelines

• Justfile PRIMARY — Use Just, not Make

• Podman not Docker — Always Podman

• License: PMPL-1.0-or-later

License

This project is licensed under the Palimpsest Meta-Project License (PMPL-1.0-or-later).

Citation

@software{echidna2026,
  title = {ECHIDNA: Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance},
  author = {Jewell, Jonathan D.A.},
  year = {2026},
  url = {https://github.com/hyperpolymath/echidna},
  license = {PMPL-1.0-or-later}
}

Contact

• GitHub Issues: https://github.com/hyperpolymath/echidna/issues

• Pull Requests: https://github.com/hyperpolymath/echidna/pulls

---

Version: 1.5.0
Status: Trust & Safety Hardening Complete
Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
Last Updated: 2026-02-08