55
66image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF Best Practices,link="https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/echidna"]
77image:https://img.shields.io/badge/License-PMPL--1.0-blue.svg[License: PMPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"]
8- image:https://img.shields.io/badge/Provers-48 -green.svg[Provers: 48 ]
9- image:https://img.shields.io/badge/Tests-613 %2B-brightgreen.svg[Tests: 613 +]
8+ image:https://img.shields.io/badge/Provers-128 -green.svg[Provers: 128 ]
9+ image:https://img.shields.io/badge/Tests-917 %2B-brightgreen.svg[Tests: 917 +]
1010image:https://api.thegreenwebfoundation.org/greencheckimage/nesy-prover.dev[Green Hosting,link="https://www.thegreenwebfoundation.org/green-web-check/?url=nesy-prover.dev"]
1111
1212*E*xtensible *C*ognitive *H*ybrid *I*ntelligence for *D*eductive *N*eural *A*ssistance
1313
14- A neurosymbolic theorem proving platform with 48 prover backends,
14+ A neurosymbolic theorem proving platform with 128 prover backends,
1515trust-hardened verification pipeline, and multi-objective proof search.
1616
1717== Leadership Position
1818
1919ECHIDNA holds a **unique leadership position** in the theorem proving ecosystem as:
2020
21- * **The only system with 48 + prover backends** (vs 1 for Isabelle, Coq, Lean, Z3, etc.)
21+ * **The only system with 128 + prover backends** (vs 1 for Isabelle, Coq, Lean, Z3, etc.)
2222* **The only system actively solving cross-prover arbitration** (mathematical object identity resolution)
2323* **The only neurosymbolic hybrid architecture** (combining AI and symbolic reasoning)
2424* **The only system with 7-stage trust pipeline** (comprehensive verification infrastructure)
2525* **The only system integrating OpenTheory + Dedukti** (universal proof exchange)
2626* **The largest vocabulary management** (992K+ terms across mathematical domains)
27- * **The most comprehensive axiom tracking** (4 danger levels across 48 provers)
27+ * **The most comprehensive axiom tracking** (4 danger levels across 128 provers)
2828* **The only Bayesian confidence scoring** (across multiple independent provers)
2929
3030Our **prevailing advantage** comes from this unique combination that no other system can match.
3131
3232== Overview
3333
34- ECHIDNA orchestrates 48 theorem provers, SMT solvers, first-order ATPs, and
34+ ECHIDNA orchestrates 128 theorem provers, SMT solvers, first-order ATPs, and
3535constraint solvers through a unified Rust core. Every proof result passes
3636through a trust-hardening pipeline that checks solver integrity, tracks axiom
3737usage, verifies proof certificates, and assigns a 5-level confidence score.
@@ -41,7 +41,7 @@ always have the final word. ECHIDNA never produces unsound proofs.
4141
4242== Features
4343
44- === 48 Prover Backends
44+ === 128 Prover Backends
4545
4646[cols="1,4", options="header"]
4747|===
@@ -66,7 +66,7 @@ always have the final word. ECHIDNA never produces unsound proofs.
6666| GLPK, SCIP, MiniZinc, Chuffed, OR-Tools
6767|===
6868
69- All 48 backends implement the `ProverBackend` trait: parse, verify, export,
69+ All 128 backends implement the `ProverBackend` trait: parse, verify, export,
7070tactic suggestion, and theorem search. File extension detection covers 30+
7171formats (`.v`, `.lean`, `.smt2`, `.tptp`, `.dfy`, `.mzn`, etc.).
7272
@@ -175,7 +175,7 @@ cd echidna
175175just build
176176# or: cargo build
177177
178- # Run all tests (613 + passing)
178+ # Run all tests (917 + passing)
179179just test
180180# or: cargo test
181181
@@ -205,7 +205,7 @@ podman run -it echidna:latest
205205[source]
206206----
207207src/rust/
208- provers/ # 48 prover backend implementations (ProverBackend trait)
208+ provers/ # 128 prover backend implementations (ProverBackend trait)
209209 verification/ # Trust-hardening subsystem
210210 portfolio.rs # SMT portfolio solving / cross-checking
211211 certificates.rs # Proof certificate checking (Alethe, DRAT/LRAT, TSTP)
@@ -268,12 +268,13 @@ println!("Verified: {}, Trust: {}", result.verified, result.trust_level);
268268
269269== Test Suite
270270
271- 613 + library tests passing (`cargo test --lib`, 2 ignored).
271+ 917 + library tests passing (`cargo test --lib --features verisim `, 2 ignored).
272272
273- * ~528 unit tests across provers, verification, integrity, executor, agent
274- * 38 integration tests (with 2 pre-existing CVC5 E2E failures tracked separately)
275- * 21 property-based tests (PropTest)
276- * Additional interface and neural integration tests
273+ * 884 tests default build (`cargo test --lib`)
274+ * 917 tests with VeriSim integration (`--features verisim`)
275+ * Smoke E2E integration tests across all prover backends
276+ * Property-based tests (PropTest)
277+ * Criterion benchmarks across all critical paths
277278
278279[source,bash]
279280----
0 commit comments