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) and Technische Universität München (Tobias Nipkow). See the Isabelle overview for a brief introduction.

Now available: Isabelle2008

Some notable improvements:

See also the cumulative NEWS.

Download & Support

Isabelle is distributed for free under the BSD license. It includes source and binary packages and browsable 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 and the Isabelle community.