-
-
Notifications
You must be signed in to change notification settings - Fork 0
Jonathan D.A. Jewell edited this page Mar 24, 2026
·
2 revisions
48+ backends including Coq, Lean 4, Idris2, Agda, Isabelle, Z3, CVC5, and many more.
Yes. Each prover runs in an isolated environment with no access to the host filesystem or network. Resource limits (CPU, memory, time) are enforced.
Trust uses a Bayesian confidence model. Proofs verified by multiple independent provers receive higher trust scores. Cross-validation across different proof systems increases confidence.
Yes — implement the ProverBackend trait and register it in backends/mod.rs. See the Guides page.