| 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 … |
| CaDiCaL |
CaDiCaL is a simplified satisfiability solver.
|
| CryptoMiniSat |
CryptoMiniSat is a SAT solver.
APIs and Bindings This tool is available through the following … |
| Gappa |
Gappa is a tool intended to help verifying and formally proving properties on numerical programs … |
| Glucose |
Glucose is a SAT solver.
|
| Lingeling |
Lingeling is a SAT solver.
|
| Metis |
[ Not Maintained Since 2020 ] Metis is an automatic theorem prover for first order logic with … |
| MiniSat |
[ Not Maintained Since 2013 ] MiniSat is a minimalistic, open-source SAT solver, developed to help … |
| ParaFROST |
ParaFROST is a parallel SAT solver with GPU-accelerated inprocessing capable of harnessing NVIDIA … |
| 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 … |
| Riss |
[ Not Maintained Since 2017 ] Riss is a SAT solving tool collection.
|
| SMT-RAT |
SMT-RAT is an SMT Real Algebra Toolbox.
APIs and Bindings This tool is available through the … |
| SPASS |
[ Closed-Source Tool ] SPASS: An Automated Theorem Prover for First-Order Logic with Equality … |
| Why3 |
Why3 is a platform for deductive program verification.
|
| Yices 2 |
Yices is an SMT solver developed by SRI International. It is widely used for checking the … |
| Z3 |
Z3 is a general-purpose theorem prover widely used for SAT & SMT solving.
APIs and Bindings This … |