PV6 tools in ProVerBPV6

PV6 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.