What is Isabelle?

Isabelle is a generic proof assistant. It allows mathematical formulas to be expressed in a formal language and provides tools for proving those formulas in a logical calculus. Isabelle is developed at University of Cambridge (Larry Paulson), Technische Universität München (Tobias Nipkow) and Université Paris-Sud (Makarius Wenzel). See the Isabelle overview for a brief introduction.

Now available: Isabelle2011-1

Notable changes:

See also the cumulative NEWS.

Download & Support

Isabelle is distributed for free under the BSD license. It includes source and binary packages and documentation, see the installation instructions. A vast collection of Isabelle examples and applications is available from the Archive of Formal Proofs.

Support is available by ample documentation, the Isabelle community Wiki, and the following mailing lists: