| ABC |
System for Sequential Logic Synthesis and Formal Verification
|
| Andromeda |
Andromeda 2 is a proof checker for user-definable dependently-typed theories.
|
| Arend |
Arend is a theorem prover and a programming language based on Homotopy Type Theory.
|
| Arvo |
[ Not Maintained Since 2015 ] Arvo is a proof assistant from the PLSE lab.
|
| Aya Prover |
A proof assistant designed for formalizing math and type-directed programming.
|
| BlazeIt |
[ Not Maintained Since 2015 ] A proof assistant.
|
| cur |
A language with static dependent-types and dynamic types, type annotations and parentheses, theorem … |
| Holbert |
Holbert is an interactive theorem prover, or proof assistant, based on higher order logic and … |
| knuckledragger |
Knuckledragger is an attempt at creating a down to earth, highly automated interactive proof … |
| Lambdapi |
Proof assistant based on the λΠ-calculus modulo rewriting
|
| LISA |
LISA is a proof assistant based on first-order logic sequent calculus and set theory.
|
| Narya |
Narya: A proof assistant for higher-dimensional type theory
|
| Otter |
[ No Longer Maintained ] Otter/Mace2 are no longer being actively developed, and maintenance and … |
| Qrhl-tool |
Qrhl-tool is an interactive theorem prover for qRHL (quantum relational Hoare logic), specifically … |
| SASyLF |
SASyLF (pronounced “Sassy Elf”) is an LF-based proof assistant specialized to checking … |
| SETHEO |
[ Not Maintained Since 2017 ] SETHEO is a theorem prover for first-order logic based on some … |
| Agda 2 |
Agda is a dependently typed programming language / interactive theorem prover.
|
| Chyp |
Chyp (pronounced “chip”) is an interactive theorem prover for symmetric monoidal … |
| Hilbert |
[ Not Maintained Since 2014 ] Hilbert is a theorem prover designed for people who don’t want … |
| Isabelle |
Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal … |
| Megalodon |
Megalodon is an open source interactive theorem prover and proof checker.
|
| Prover9 |
Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for … |
| PVS |
PVS is a mechanized environment for formal specification and verification. PVS consists of a … |
| Rocq |
A trustworthy, industrial-strength interactive theorem prover and dependently-typed programming … |
| Whiley Theorem Prover |
The Whiley Theorem Prover (WyTP) is an automatic and interactive theorem prover designed to … |
| Abella |
Abella is an interactive theorem prover based on lambda-tree syntax.
|
| BEAGLE |
Beagle is an automated theorem prover for first-order logic with equality over linear … |
| Bitwuzla |
Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size … |
| Boolector |
[ Not Maintained Since 2024 ] Boolector is a Satisfiability Modulo Theories (SMT) solver for the … |
| cvc4 |
[ Not Maintained Since 2021 ] cvc4 is an automatic theorem prover for SMT problems. It is succeeded … |
| cvc5 |
cvc5 is an automatic theorem prover for SMT problems.
|
| E |
E is a theorem prover for full first-order logic (and now monomorphic higher-order logic) with … |
| Gappa |
Gappa is a tool intended to help verifying and formally proving properties on numerical programs … |
| LEAN |
cvc5 is an automatic theorem prover for SMT problems.
|
| Metis |
[ Not Maintained Since 2020 ] Metis is an automatic theorem prover for first order logic with … |
| Princess |
Princess is a theorem prover (aka SMT Solver) for Presburger arithmetic with uninterpreted … |
| Profound |
[ Not Maintained Since 2011 ] Profound is an experiment in subformula linking as an interaction … |
| pyPL |
pyPL is a naive model generator, model checker and theorem prover.
|
| SPASS |
[ Closed-Source Tool ] SPASS: An Automated Theorem Prover for First-Order Logic with Equality … |
| STP |
STP is a constraint solver for quantifier-free bitvectors.
APIs and Bindings This tool is available … |
| Vampire |
Vampire is a theorem prover.
|
| Why3 |
Why3 is a platform for deductive program verification.
|
| Z3 |
Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.
APIs and Bindings This … |
| Zipperposition |
Zipperposition is an automated theorem prover for first-order logic with equality and theories.
|