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.

Test version for VSL 2014 (Isabelle tutorial)

See Isabelle2014-RC0. Participants of the Isabelle tutorial at Vienna 13-Jul-2014 should have this installed on their machine.

Now available: Isabelle2013-2

Some highlights:

See also the cumulative NEWS.

Distribution & Support

Isabelle is distributed for free under the BSD license. It includes source and binary packages and documentation, see the detailed 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, Stack Overflow, and in particular the following mailing lists: