The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As a Logic for Computable Functions (LCF) style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring, yet supporting, explicit proof objects.

Isabelle is available inside a flexible system framework allowing for logically safe extensions, which comprise both theories and implementations for code-generating, documenting, and specific support for a variety of formal methods. It can be seen as an integrated development environment (IDE) for formal methods. In recent years, a substantial number of theories and system extensions have been collected in the Isabelle Archive of Formal Proofs (Isabelle AFP).

Isabelle was named by Lawrence Paulson after Gérard Huet's daughter.

The Isabelle theorem prover is free software, released under the revised BSD license.

Features<!--'Intelligible semi-automated reasoning', 'Isar (Isabelle)', 'Locale (Isabelle)', 'Metis (theorem prover)', 'Nitpick (Isabelle)', 'Nunchaku (Isabelle)', and 'Sledgehammer (Isabelle)' redirect here-->

Isabelle is generic: it provides a meta-logic (a weak type theory), which is used to encode object logics like first-order logic (FOL), higher-order logic (HOL) or Zermelo–Fraenkel set theory (ZFC). The most widely used object logic is Isabelle/HOL, although significant set theory developments were completed in Isabelle/ZF. Isabelle's main proof method is a higher-order version of resolution, based on higher-order unification.

Though interactive, Isabelle features efficient automatic reasoning tools, such as a term rewriting engine and a tableaux prover, various decision procedures, and, through the Sledgehammer<!--boldface per WP:R#PLA--> proof-automation interface, external satisfiability modulo theories (SMT) solvers (including CVC4) and resolution-based automated theorem provers (ATPs), including E, SPASS, and Vampire (the Metis<!--boldface per WP:R#PLA--> proof method reconstructs resolution proofs generated by these ATPs). It also features two model finders (counterexample generators): Nitpick<!--boldface per WP:R#PLA--> and Nunchaku<!--boldface per WP:R#PLA-->.

Isabelle features locales<!--boldface per WP:R#PLA--> which are modules that structure large proofs. A locale fixes types, constants, and assumptions within a specified scope

On the other hand, declarative proofs (supported by Isabelle's proof language, Isar) specify the actual mathematical operations to be performed, and are therefore more easily read and checked by humans.

For example, a declarative proof by contradiction in Isar that the square root of two is not rational can be written as follows.

<div style="font-family: monospace, monospace;">

sqrt2_not_rational:

?x =

m n :: nat

sqrt_rat: lowest_terms:

(rule Rats_abs_nat_div_natE)

(auto simp add: power2_eq_square)

eq: of_nat_eq_iff power2_eq_square fastforce

simp

simp

-

k ..<!--The two dots refer to a complete proof of this claim-->

eq simp

simp

simp

(rule gcd_greatest)

lowest_terms simp

False odd_one blast

</div>

Applications

Isabelle has been used to aid formal methods for the specification, development and verification of software and hardware systems.

Isabelle has been used to formalize numerous theorems from mathematics and computer science, like Gödel's completeness theorem, Gödel's theorem about the consistency of the axiom of choice, the prime number theorem, correctness of security protocols, and properties of programming language semantics. Many of the formal proofs are, as mentioned, maintained in the Archive of Formal Proofs, which contains (as of 2019) at least 500 articles with over 2 million lines of proof in total.

  • In 2009, the L4.verified project at NICTA produced the first formal proof of functional correctness of a general-purpose operating system kernel: the seL4 (secure embedded L4) microkernel. The proof is constructed and checked in Isabelle/HOL and comprises over 200,000 lines of proof script to verify 7,500 lines of C. The verification covers code, design, and implementation, and the main theorem states that the C code correctly implements the formal specification of the kernel. The proof uncovered 144 bugs in an early version of the C code of the seL4 kernel, and about 150 issues in each of design and specification.
  • The definition of the programming language Lightweight Java was proven type-sound in Isabelle.

Alternatives

Several languages and systems provide similar functions:

  • Agda, written in Haskell
  • Rocq (formerly named Coq), written in OCaml
  • Lean, written in Lean and C++
  • LEGO, written in Standard ML of New Jersey
  • Mizar system, written in Free Pascal
  • Metamath, written in ANSI C
  • Prover9, written in C, with a GUI written in Python
  • Twelf, written in Standard ML

Notes

References

Further reading

  • Lawrence C. Paulson, "The Foundation of a Generic Theorem Prover", Journal of Automated Reasoning, Volume 5, Issue 3 (September 1989), pages: 363–397, .
  • Lawrence C. Paulson and Tobias Nipkow, "Isabelle Tutorial and User's Manual", 1990.
  • M. A. Ozols, K. A. Eastaughffe, and A. Cant, "DOVE: A Tool for Design Oriented Verification and Evaluation", Proceedings of AMAST 97, M. Johnson, editor, Sydney, Australia. Lecture Notes in Computer Science (LNCS) Vol. 1349, Springer Verlag, 1997.
  • Tobias Nipkow, Lawrence C. Paulson, Markus Wenzel, "Isabelle/HOL – A Proof Assistant for Higher-Order Logic", 2020.
  • Isabelle on Stack Overflow
  • The Archive of Formal Proofs
  • IsarMathLib