Skip to content

CLAUDE.md

Latest commit

 

History

History
178 lines (145 loc) · 7.64 KB

CLAUDE.md

File metadata and controls

178 lines (145 loc) · 7.64 KB

CLAUDE.md

This document provides guidelines and context for working with Claude Code on the ECHIDNA project.

Project Overview

ECHIDNA (Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance) is a trust-hardened neurosymbolic theorem proving platform supporting 48 prover backends with a comprehensive verification pipeline.

Repository: https://github.com/hyperpolymath/echidna Version: 2.1.0 License: PMPL-1.0-or-later

Repository Structure

echidna/
├── src/
│   ├── rust/               # Rust core (48 provers, trust pipeline)
│   │   ├── provers/        # 30 prover backend implementations
│   │   ├── verification/   # Trust pipeline (portfolio, certificates, axioms, confidence, mutation, pareto, statistics)
│   │   ├── 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)
│   │   ├── gnn/            # GNN integration (graph construction, embeddings, client, guided search)
│   │   ├── neural.rs       # Neural premise selection (text-based, complements GNN)
│   │   ├── aspect.rs       # Aspect tagging
│   │   ├── core.rs         # Core types (Term, ProofState, Tactic, Goal)
│   │   ├── 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
│   ├── interfaces/         # API interfaces (workspace members)
│   │   ├── graphql/        # GraphQL (async-graphql, port 8081)
│   │   ├── grpc/           # gRPC (tonic, port 50051)
│   │   └── rest/           # REST (axum + OpenAPI, port 8000)
│   ├── julia/              # Julia ML components
│   ├── rescript/           # ReScript+Deno UI (33 files)
│   └── mercury/            # Mercury/Logtalk logic (optional)
├── .machine_readable/      # SCM files (STATE.scm, META.scm, ECOSYSTEM.scm)
├── .github/workflows/      # 17 CI/CD workflows
├── Cargo.toml              # Rust workspace root
├── Justfile                # Primary build system
└── Containerfile           # Podman container

Working with Claude Code

General Guidelines

  1. Code Quality: Maintain high code quality standards with proper error handling, tests, and documentation
  2. Git Workflow: Follow conventional commit messages and keep commits atomic
  3. Security: Be vigilant about security vulnerabilities
  4. Dependencies: Document all dependencies and their purposes

Commit Message Format

Follow conventional commit format:

  • feat: - New features
  • fix: - Bug fixes
  • docs: - Documentation changes
  • refactor: - Code refactoring
  • test: - Adding or updating tests
  • chore: - Maintenance tasks

Project-Specific Context

Tech Stack

  • Rust: Core logic, 48 prover backends, trust pipeline, CLI, REPL, API servers
  • Julia: ML inference (tactic prediction, premise selection, port 8090)
  • ReScript + Deno: UI components (33 files, zero TypeScript)
  • Chapel: Optional parallel proof dispatch

Prover Support (48 Total - ALL IMPLEMENTED)

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

Trust & Safety Pipeline

The v1.5 trust hardening added:

  1. Solver binary integrity verification (SHAKE3-512 + BLAKE3)
  2. SMT portfolio solving / cross-checking
  3. Proof certificate checking (Alethe, DRAT/LRAT, TSTP)
  4. Axiom usage tracking (4 danger levels: Safe, Noted, Warning, Reject)
  5. Solver sandboxing (Podman, bubblewrap, none)
  6. 5-level trust hierarchy for confidence scoring
  7. Mutation testing for specifications
  8. Prover dispatch pipeline
  9. Cross-prover proof exchange (OpenTheory, Dedukti)
  10. Pareto frontier computation for multi-objective proof search
  11. Statistical confidence tracking with Bayesian timeout estimation

Key Components

  • src/rust/provers/mod.rs: ProverBackend trait, ProverKind enum (48 variants), ProverFactory
  • src/rust/dispatch.rs: Full trust-hardening dispatch pipeline
  • src/rust/verification/: Portfolio, certificates, axiom tracker, confidence, mutation, pareto, statistics
  • src/rust/integrity/: Solver binary integrity (SHAKE3-512, BLAKE3)
  • src/rust/executor/: Sandboxed solver execution
  • src/rust/exchange/: OpenTheory, Dedukti proof exchange
  • src/rust/core.rs: Core types (Term, ProofState, Tactic, Goal, Context, Theorem)
  • src/rust/gnn/: GNN integration (graph construction, embeddings, inference client, guided search)
  • src/rust/agent/: Agentic proof search (actor model)

Current Status

Completed (v2.0.0):

  • 48/48 prover backends across 10 tiers
  • Trust & safety hardening (13 tasks complete)
  • 638+ tests passing (528 unit + 38 integration + 21 property + interface)
  • 3 API interfaces (GraphQL, gRPC, REST) with real prover backend invocation
  • Agda meta-checker: 30+ formally verified trust pipeline properties
  • Criterion benchmarks: 13 functions covering all critical paths
  • FFI bridge: complete C-compatible API for all 48 provers
  • Julia ML layer (logistic regression, MRR 0.66)
  • 26 CI/CD workflows (including Agda meta-checker)
  • Zig FFI layer (4 shared libraries)
  • Idris2 ABI formal proofs (16 modules, zero believe_me)
  • 0 clippy warnings, 0 compiler errors on stable Rust

v2.1 (GNN Integration):

  • GNN proof graph construction (7 node kinds, 8 edge kinds)
  • 32-dim local term embeddings + GNN inference client
  • GNN-guided proof search (hybrid GNN + symbolic scoring)
  • Julia /gnn/rank endpoint with cosine fallback
  • Idris2 formal proofs: 7 GNN properties (0 believe_me)
  • 28 new tests, 0 clippy warnings

Next (v2.2+):

  • Train GNN/Transformer on larger corpus (Flux.jl)
  • Chapel → Rust C FFI bridge
  • Tamarin/ProVerif bridge

Useful Commands

# Build System (Justfile is PRIMARY)
just build              # Build the project
just test               # Run tests (638+)
just check              # Run all quality checkers

# Cargo commands
cargo build             # Build Rust code
cargo test              # Run all tests
cargo test --lib        # Unit tests only (232)
cargo test --test integration_tests  # Integration tests (38)

# Container Management (Podman, not Docker)
podman build -f Containerfile .   # Build container
podman run echidna                # Run container

# Quality Checks
cargo clippy                      # Rust lints
cargo fmt --check                 # Format check

Critical Constraints

  • NO PYTHON - use Julia for ML/data, Rust for systems, ReScript for apps
  • RSR/CCCP Compliance Required - follow Rhodium Standard Repository guidelines
  • Justfile PRIMARY - never use Make or other build systems
  • Podman not Docker - always use Podman for containers
  • License: PMPL-1.0-or-later (not AGPL, not dual MIT/Palimpsest)
  • Author: Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk

Last Updated: 2026-03-23 Maintained By: Jonathan D.A. Jewell j.d.a.jewell@open.ac.uk