PV6 tools in ProVerBPV6PV6 tools can handle different user-written specifications, encode a wide range of different formulae for properties, and are capable of producing proofs of such properties together with inferring the correctness of such proofs.
- ACL2 (a full-fledged language to write specs and prove their properties)
- Cameleer (generates a proof of desired properties, can be used interactively)
- Coq (interactive theorem prover)
- HOL (interactive theorem prover)
- Isabelle-HOL (interactive theorem prover)
- Ivy (deductively or inductively proves or helps prove program properties)
- KeY (generates a proof of desired properties, can proceed interactively if stuck otherwise)
- Lean (interactive theorem prover)
- ProofPower (theorem prover)
- Rodin (theorem prover)
- Tinker (interactive theorem prover with various backends)
- Vampire (can produce proofs for theorems in first order logic)
- veriT (produces a proof for satisfiability of a formula)
13 items on this list.