CProver is a tool for the formal verification of ANSI-C programs and hardware designs given in a description language such as Verilog or VHDL.

CheckMate is a verification tool for hybrid dynamic systems, that is, dynamic systems with both discrete and continuous state variables. Hybrid systems often arise in computer-control systems where the discrete dynamics corresponds to the control logic and the continuous dynamics corresponds to the physical system being controlled.

Model Checkers such as SMV have been applied successfully in many different domains, e.g., hardware and protocol verification.

Ymer is a tool for verifying probabilistic transient properties of continuous-time Markov chains (CTMCs) and generalized semi-Markov processes (GSMPs). Properties are expressed using the Continuous Stochastic Logic (CSL).

SF2SMV uses Model Checking to formally verify Stateflow diagrams.

UCLID is a tool for modeling and verifying systems at a term level, with both Boolean and integer data types, uinterpreted functions, and restricted forms of integer arithmetic. It consists of a modeling language, a symbolic simulator, and a set of decision procedures. It can be used in three modes: as a bounded property checker, to verify pipelined processors, and to prove inductive invariants.