A wide range of mature formal modeling and verification tools is available today, including the model finding tool Alloy, the model checker nuSMV, code verification tools like VCC and KeY, or interactive theorem provers like Isabelle/HOL or Coq.

Each project comes with different requirements regarding the kinds of models and specifications to construct, the properties to verify, as well as scale and complexity of the targeted artifacts. Therefore, there is no one method and tool that will fit all projects in a reliable and cost-effective way. The success of a formal assurance project strongly depends on carefully choosing an appropriate method and tool set that will scale without imposing an unnecessary and costly burden on model development and verifcation.