Tools 

SMT

Bitwuzla
Bitwuzla
SMT Solver
Bitwuzla is an award-winning Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations.
View on GitHub
Boolector
Boolector
SMT Solver
Boolector is an award-winning Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions and their combinations.
View on GitHub
cvc5
cvc5
SMT Solver
cvc5 is an award-winning automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. cvc5 is the successor of CVC4.
View on GitHub
ddsmt
ddsmt
Delta Debugger for SMT-LIB
ddSMT is a delta debugger for input in the SMT-LIB language and its dialects and extensions. It serves as an input minimizer for SMT-LIB(-like) input that triggers interesting behavior for a given command.
View on GitHub
Smt-Switch
Smt-Switch
A Solver-Agnostic C++ API for SMT Solving
Smt-Switch provides abstract C++ classes which can be implemented by different SMT solvers. Our model checker Pono is built using Smt-Switch.
View on GitHub

Model Checking

Pono
Pono
SMT-Based Model Checker
Pono is a flexible and extensible SMT-based model checker that leverages word-level reasoning. 'Pono' is the Hawaiian word for proper, correct, or goodness.

Pono is the successor of our model checkers CoSA and CoSA2.
View on GitHub

Neural Network Verification

Marabou
Marabou
SMT-Based Framework for Verifying Deep Neural Networks
Marabou is an SMT-based tool that can answer queries about the properties of a neural network by transforming these queries into constraint satisfaction problems.
View on GitHub

Deprecated Tools

Cosa
Cosa
CoreIR Symbolic Analyzer
CoSA is an SMT-based symbolic model checker for hardware designs. It is succeeded by Pono.
View on GitHub
Cosa2
Cosa2
CoreIR Symbolic Analyzer
CoSA2 is an SMT-based symbolic model checker for hardware designs. It is succeeded by Pono.
View on GitHub
CVC4
CVC4
SMT Solver
CVC4 is an award-winning automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It is succeeded by cvc5.
View on GitHub