Repository navigation
There is no single number, and that is the honest answer rather than a dodge:
the tree contains 141 ProverKind variants across 105 backend
implementation files, of which 102 provide suggest_tactics. Which figure
is "the" count depends on what you are counting.
docs/PROVER_COUNT.adoc
is canonical and ships the commands that reproduce each one.
12 core backends are exposed by the default REST API, mirroring
ProverKind::all_core(): Agda, Coq, Lean 4, Isabelle/HOL, Z3, CVC5, Metamath,
HOL Light, Mizar, PVS, ACL2, HOL4. Everything else is reachable via explicit
ProverKind selection in CLI / REPL / GraphQL.
The full tier table lives in docs/PROVER_COUNT.adoc.
Yes. Each prover runs in Podman or bubblewrap with no host filesystem or network access. Resource limits (CPU, memory, wall time) are enforced per DispatchConfig. See src/rust/executor/.
Five-tier Bayesian confidence model (src/rust/verification/confidence.rs). Proofs verified by multiple independent provers receive higher trust. Cross-prover certificate verification (Alethe / DRAT-LRAT / TSTP, replayed independently) elevates trust further. Solver binaries are SHAKE3-512 + BLAKE3 integrity-checked against config/solver-manifest.toml before invocation.
Yes. Implement the ProverBackend trait in src/rust/provers/your_prover.rs, add a variant to ProverKind, register in ProverFactory, and add fixtures under tests/. See Guides for the step-by-step.
Julia sidecar (port 8090). A GNN ranks premises; a logistic regression head suggests tactics. Both can be retrained from accumulated proof outcomes stored in VeriSimDB. The architecture is "ML suggests; provers verify" — a wrong suggestion costs a CPU cycle, not soundness.
See docs/ARCHITECTURE.adoc for the data flow.
No. The repo wins when the wiki and the in-repo docs disagree. The wiki is a navigation aid pointing at the canonical sources. Pages here are refreshed periodically but lag the repo.
Canonical sources of truth:
-
CLAUDE.mdfor codebase orientation -
.machine_readable/descriptiles/STATE.a2mlfor current state -
docs/ROADMAP.adocfor direction
MPL-2.0 for the code, CC-BY-SA-4.0 for the documentation.
| Part | Licence |
|---|---|
Code — src/, crates/, ffi/, proofs/, spark/, verification/, build system, CI |
MPL-2.0 |
Machine-readable specification surface — .machine_readable/, package/container manifests, OCI image labels |
MPL-2.0 |
Documentation — docs/, top-level .md / .adoc
|
CC-BY-SA-4.0 |
echidna-playground/ — the Coq-Jr sub-project |
MPL-2.0 (never relicensed) |
MPL-2.0 is file-level copyleft: if you modify one of ECHIDNA's files and distribute it, that file stays open under MPL-2.0; combining ECHIDNA with your own code places no obligation on the rest of your work. The playground keeps MPL because it carries contributions from Coq-Jr Contributors, and relicensing someone else's contribution needs their consent.
Files that previously offered Palimpsest-0.6 now carry MPL-2.0: the
Palimpsest Licence is MPL-2.0 with ethical provisions layered on top, so
MPL-2.0 is the faithful reduction when that layer is not being asserted.
Licence history: dual MIT/Palimpsest-0.6 → MPL-2.0 → AGPL-3.0-or-later for
application code with the specification surface held at MPL-2.0 (2026-08) →
MPL-2.0 throughout (re-ruled 2026-10-01). Anything describing application code
as AGPL predates that;
LICENSE and
NOTICE are
authoritative.
See SECURITY.md and .well-known/security.txt. Do not disclose publicly until addressed.
17 adapters as of the 2026-06-01 saturation campaign (src/rust/corpus/<name>.rs):
agda, coq, lean, idris2, isabelle, metamath, mizar, hol_light, hol4, dafny, why3, fstar, acl2_books, tptp, smtlib, proofnet, minif2f.
The first four shipped pre-2026-04; the other 13 landed in the saturation campaign. Each adapter is pub fn ingest(root: &Path) -> Result<Corpus> and surfaces hazard flags (postulate, believe_me, sorry, cheat, Admitted, …) via AxiomUsage.
Full table with file extensions, upstream source URLs, and hazard flags: docs/CORPUS-ADAPTERS.adoc.
| Arbiter | Module | Output | Strength |
|---|---|---|---|
| Portfolio | src/rust/verification/portfolio.rs |
Categorical agreement summary | Simple majority across N solvers; no calibration needed. |
| Bayesian | src/rust/verification/bayesian_arbiter.rs |
PosteriorVerdict (probabilities + Shannon entropy) |
Calibrated per-prover precision/FPR; uses log-odds accumulation. |
| Dempster-Shafer | src/rust/verification/dempster_shafer.rs |
BeliefPlausibility over VerdictSet, or ArbiterError::HighConflict(k)
|
Models ignorance explicitly; refuses to commit when conflict is too high. |
| Pareto | src/rust/verification/pareto_arbiter.rs |
ParetoDecision over multi-axis outcomes |
Multi-objective (time, memory, certificate-size, trust-tier) — returns non-dominated set, not a single verdict. |
Guides has a "Picking an arbitration mechanism" walkthrough with motivating examples.
No. They are offline-resilient enhancements to the synonym layer. load_cross_prover_dicts (src/rust/suggest/synonyms.rs) silently returns empty SynonymTables if the underscore-prefix TOMLs (_msc2020.toml, _wordnet_math.toml, _conceptnet_seed.toml) are missing from data/synonyms/. Per-prover synonym lookup still works; cross-prover by_semantic_class queries just return fewer hits.
Yes. TPTP is supported on two surfaces:
-
Corpus ingest —
src/rust/corpus/tptp.rswalks a directory of*.p/*.tptpfiles and indexes annotated formulas (fof,cnffully supported;tff/thfrecognised but not translated). -
Exchange —
src/rust/exchange/tptp.rsparses, emits, and best-effort-translates between TPTP and SMT-LIB v2 for cross-prover interop. Vampire, E, SPASS, Princess, iProver, Twee all consume TPTP natively.
The src/rust/exchange/smtcoq.rs module is a stub bridge — its module docs say so explicitly. It supplies enough Alethe / LFSC / DRAT parser surface to drive downstream consumers and emits an honest skeleton with (* TODO: SMTCoq integration not yet wired *) markers, but does not invoke the actual SMTCoq Coq plugin to replay the proof in the Coq kernel.
A full bridge would require the upstream SMTCoq binary on PATH and would replay Z3 / veriT / CVC4 unsat proofs against Coq for kernel-level re-checking. That's gated on the upstream SMTCoq plugin and is out of scope for the current module. Downstream callers can detect the stub status by grepping the emitted skeleton for the TODO markers before trusting the output.
Two complementary surfaces:
-
docs/architecture/VERISIM-ER-SCHEMA.adoc— the formal entity-relationship schema for the VeriSim shared-state model (entities, relations, cardinalities, invariants). -
crates/echidna-wire/schemas/verisim_er.capnp— the Cap'n Proto wire schema that implements it.
The 8-modality octad emission layer (src/rust/corpus/octad.rs) is the load-bearing producer; any corpus from any adapter can emit octads conforming to this schema.