Formal Methods Tools

BSD

Tool Description
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.
Vampire Vampire is a theorem prover.
veriT veriT is an SMT solver developed by LORIA and ULiege. It supports a wide range of theories and is …
Zipperposition Zipperposition is an automated theorem prover for first-order logic with equality and theories.