Automated versus Manual Proof Tools

There are two main styles of mechanised proof tool:

• Automatic Proof Tools require no manual input. The main example is/was the model checker. Their grander descendant, the SAT-modulo checkers (SMT tool) expands the application space for automatic proof.
• Theorem Provers hold a database of axioms, logic rules and already derived theorems. Manual guidance is used to request which rule to apply to the current theorem set to produce further theorems. Eventually the required result can hopefully be found. A lot of semi-automatic application of rules is commonly supported (called tactics.) Previous proofs can be saved as tactics for replay in the current proof.

Contemporary, industrial SoC design only uses fully automated provers, whereas research in specification and verification often uses manually-guided provers where the computer may make suggestions about proof steps buts its main role is to check the result has been derived without a false step.

Well-known model checkers are SMV and Spin. Yices and Z3 are SMT solvers.

Well-known theorem provers are HOL, Isabelle, ACL2 and Coq.

Cadence JasperGold is commonly used in industry and contains many tools in this space.