Isabelle

Isabelle is a generic proof assistant developed by Larry Paulson at the University of Cambridge and Tobias Nipkow at TU Munich. Unlike proof assistants built on a single fixed logic, Isabelle is a framework for implementing and reasoning in multiple logics, with Isabelle/HOL — higher-order logic — being the most widely used instantiation. The generic architecture means that Isabelle can be instantiated with classical logic, constructive logic, or even custom domain-specific logics, though in practice the vast majority of verification work uses Isabelle/HOL.

The distinguishing feature of Isabelle is its combination of automation and human guidance. The proof language, Isar, supports structured proofs that are readable independently of the theorem prover, resembling the informal proofs mathematicians write on paper. At the same time, Isabelle provides powerful automated tactics — sledgehammer, which invokes external automated theorem provers, and nitpick, which searches for counterexamples — that can discharge proof obligations without manual intervention. This balance between readability and automation has made Isabelle the tool of choice for large-scale software verification, including the seL4 microkernel and the CompCert compiler.

Isabelle's philosophy is pragmatic rather than foundational. It does not seek to replace informal mathematics with a single formal system; it seeks to make formal verification accessible to engineers and mathematicians who do not specialize in logic. The cost of this pragmatism is that Isabelle/HOL is less expressive than the dependent type theories of Coq or Agda; it cannot encode proofs as programs in the same way, and its logic is classical rather than constructive. The benefit is that it scales to verification projects involving hundreds of thousands of lines of proof, and its automation reduces the cost of formalization to levels that industry can afford.