Isabelle/HOL is a popular proof assistant based on higher-order logic. It owes its success to its ease of use and powerful automation. Much of the automation is performed by external tools: The metaprover Sledgehammer relies on automatic theorem provers for its proof search, and the counterexample generator Nitpick relies on SAT solvers. Together with the Isar structured proof format and a new asynchronous user interface, these tools have radically transformed the Isabelle user experience. Recently, Isabelle has been used to verify the seL4 microkernel, to formalize the Java and C++ memory models, and even to prove the existence of God.

Homepage J. Blanchette