Skip to content

FAQ.md

Latest commit

 

History

History
44 lines (24 loc) · 2.97 KB

FAQ.md

File metadata and controls

44 lines (24 loc) · 2.97 KB
Raw

FAQ

How many provers are supported?

128 total ProverKind variants: 89 external prover bindings plus 39 TypeChecker disciplines routed via TypedWasm Sigma.

Of these, 12 core are exposed by the default REST API: Coq/Rocq, Lean 4, Agda, Isabelle/HOL, Idris 2, F*, Z3, CVC5, Alt-Ergo, Dafny, Vampire, E Prover. The remaining 116 are reachable via explicit ProverKind selection in CLI / REPL / GraphQL.

The full tier table lives in docs/PROVER_COUNT.md.

Are proofs sandboxed?

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/.

How is trust scored?

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.

Can I add my own prover?

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.

What's the ML layer?

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.md for the data flow.

Is the wiki authoritative?

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:

Why AGPL-3.0-or-later?

Estate-wide policy decision (co-dev alignment). The project migrated from MPL-2.0 to AGPL-3.0-or-later on 2026-05-27 (#112); prior to MPL-2.0 it had been dual MIT/Palimpsest-0.6. NOTICE and LICENSE reflect the current state.

How do I report a security issue?

See SECURITY.md and .well-known/security.txt. Do not disclose publicly until addressed.