ECHIDNA

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

A neurosymbolic theorem proving platform supporting 12 theorem provers with aspect tagging, OpenCyc integration, and DeepProbLog probabilistic logic.

Features

• 12 Theorem Prover Support: Universal backend supporting Agda, Coq/Rocq, Lean, Isabelle, Z3, CVC5, Metamath, HOL Light, Mizar, PVS, ACL2, and HOL4

• Neurosymbolic AI: Neural proof synthesis combined with symbolic verification

• Aspect Tagging: Intelligent proof categorization and analysis

• OpenCyc Integration: Common sense reasoning with ontological knowledge

• DeepProbLog: Probabilistic logic programming for uncertain reasoning

• 4-Language Architecture: Rust (core), Julia (ML), ReScript (UI), Mercury/Logtalk (logic)

Quick Start

Prerequisites

• Rust 1.75 or later

• Julia 1.10 or later

• Deno 1.40 or later (for ReScript)

• Podman (NOT Docker)

• Just command runner

Installation

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

# Build the project
just build

# Run tests
just test

# Run ECHIDNA
just run

Using Podman Container

# Build container
podman build -f Containerfile -t echidna:latest .

# Run container
podman run -it echidna:latest

Architecture

Prover Tiers

Tier 1 (6 provers): - Agda - Dependent type theory - Coq/Rocq - Interactive theorem prover - Lean - Functional programming and proving - Isabelle - Higher-order logic - Z3 - SMT solver - CVC5 - SMT solver

Tier 2 (3 provers): - Metamath - Plain text verifier - HOL Light - Classical higher-order logic - Mizar - Mathematical vernacular

Tier 3 (2 provers): - PVS - Specification and verification - ACL2 - Applicative Common Lisp

Tier 4 (1 prover): - HOL4 - Higher-order logic

Technology Stack

• Rust: Core logic, FFI, WASM compilation

• Julia: Machine learning components (NO Python allowed!)

• ReScript + Deno: User interface

• Mercury/Logtalk: Optional logic reservoir

Key Components

• src/rust/provers/: Complete Rust prover implementations

• Aspect Tagging System: Proof classification and analysis

• Neural Solver: ML-based proof synthesis

• Universal Prover Abstraction: Unified interface for all 12 provers

Usage

Basic Theorem Proving

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

let backend = ProverFactory::create(ProverKind::Agda, config)?;
let state = backend.parse_string("module T where\nid : {A : Set} → A → A\nid x = x").await?;
let verified = backend.verify_proof(&state).await?;

Using Multiple Provers

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

// Try multiple provers
let provers = vec![ProverKind::Lean, ProverKind::Coq, ProverKind::Z3];
for kind in provers {
    let backend = ProverFactory::create(kind, config.clone())?;
    if let Ok(state) = backend.parse_string(theorem).await {
        if backend.verify_proof(&state).await.unwrap_or(false) {
            println!("Proved with {:?}", kind);
            break;
        }
    }
}

Neural Proof Synthesis

using EchidnaML

# Train neural model
model = train_proof_synthesizer(training_data)

# Generate proof candidates
candidates = synthesize_proofs(model, theorem)

# Verify with symbolic prover
for candidate in candidates
    if verify_proof(candidate)
        return candidate
    end
end

Development

Building from Source

# Install dependencies
just deps

# Build all components
just build

# Build specific component
just build-rust
just build-julia
just build-rescript

Running Tests

# Run all tests
just test

# Run Rust tests
cargo test

# Run unit tests only
cargo test --lib

# Run integration tests
cargo test --test integration_tests

Quality Checks

# Run all quality checks
just check

# Individual checks
just lint          # REUSE, rustfmt, clippy
just security      # Trivy, cargo-audit
just coverage      # Test coverage

Documentation

• Contributing Guidelines

• Code of Conduct

• Security Policy

• Changelog

• API Documentation

Current Status

Completed: - All 12 prover backends implemented - 99 unit tests passing - 38 integration tests passing - RSR/CCCP compliance templates - Complete Rust trait system

In Progress: - Neural/ML integration (Julia components) - UI implementation (ReScript + Deno)

Contributing

We welcome contributions! Please see CONTRIBUTING.md for guidelines.

Critical Constraints

• NO PYTHON - Use Julia for all ML code

• RSR/CCCP Compliance - Follow Rhodium Standard Repository guidelines

• Justfile PRIMARY - Use Just, not Make

• Podman not Docker - Always use Podman

• Dual Licensing - MIT + Palimpsest v0.6

License

This project is dual-licensed under:

• MIT License

• Palimpsest License v0.6

See NOTICE for complete license information.

Citation

If you use ECHIDNA in your research, please cite:

@software{echidna2025,
  title = {ECHIDNA: Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance},
  author = {ECHIDNA Project Contributors},
  year = {2025},
  url = {https://github.com/hyperpolymath/echidna},
  license = {MIT AND Palimpsest-0.6}
}

Acknowledgments

• Built on the shoulders of the theorem proving community

• See AUTHORS.md for contributor list

Contact

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

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

• Security: [email protected]

---

Version: 0.1.0 Status: Active Development Last Updated: 2026-01-10