Isabelle
Isabelle–jEdit running onmacOS
Original author	Lawrence Paulson
Developers	University of Cambridge Technical University of Munich, et al.
Initial release	1986; 39 years ago (1986)[1]
Stable release	Isabelle2025 / March 2025; 7 months ago (2025-03)
Written in	Standard ML,Scala
Operating system	Linux,Windows,macOS
Type	Mathematics
License	BSD
Website	isabelle.in.tum.de

TheIsabelle^[a]automated theorem prover is ahigher-order logic (HOL) theorem prover, written inStandard ML andScala. As aLogic 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 offormal methods. It can be seen as anintegrated development environment (IDE) for formal methods. In recent years, a substantial number of theories and system extensions have been collected in the IsabelleArchive of Formal Proofs (Isabelle AFP).^[2]

Isabelle was named byLawrence Paulson afterGérard Huet's daughter.^[3]

The Isabelle theorem prover isfree software, released under the revisedBSD license.

Isabelle is generic: it provides ameta-logic (a weaktype theory), which is used to encode object logics likefirst-order logic (FOL),higher-order logic (HOL) orZermelo–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 ofresolution, based on higher-orderunification.

Though interactive, Isabelle features efficient automatic reasoning tools, such as aterm rewriting engine and atableaux prover, various decision procedures, and, through theSledgehammer proof-automation interface, externalsatisfiability modulo theories (SMT) solvers (includingCVC4) andresolution-basedautomated theorem provers (ATPs), includingE,SPASS, andVampire (theMetis^[b] proof method reconstructs resolution proofs generated by these ATPs).^[4] It also features twomodel finders (counterexample generators):Nitpick^[5] andNunchaku.^[6]

Isabelle featureslocales which are modules that structure large proofs. A locale fixes types, constants, and assumptions within a specified scope^[5] so that they do not have to be repeated for everylemma.

Isar ("intelligible semi-automated reasoning") is Isabelle's formal proof language. It is inspired by theMizar system.^[5]

Isabelle allows proofs to be written in two different styles, theprocedural and thedeclarative. Procedural proofs specify a series oftactics (theorem provingfunctions/procedures) to apply. While reflecting the procedure that a human mathematician might apply to proving a result, they are typically hard to read as they do not describe the outcome of these steps. This style is "considered harmful" in the Isabelle documentation.^[7]

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 declarativeproof by contradiction in Isar thatthe square root of two is not rational can be written as follows.

theorem sqrt2_not_rational:"sqrt 2 ∉ ℚ"prooflet ?x ="sqrt 2"assume"?x ∈ ℚ"thenobtain m n :: natwhere    sqrt_rat:"¦?x¦ = m / n"and lowest_terms:"coprime m n"by (rule Rats_abs_nat_div_natE)hence"m^2 = ?x^2 * n^2"by (auto simp add: power2_eq_square)hence eq:"m^2 = 2 * n^2"using of_nat_eq_iff power2_eq_squareby fastforcehence"2 dvd m^2"by simphence"2 dvd m"by simphave"2 dvd n"proof -from‹2 dvd m›obtain kwhere"m = 2 * k" ..with eqhave"2 * n^2 = 2^2 * k^2"by simphence"2 dvd n^2"by simpthus"2 dvd n"by simpqedwith‹2 dvd m›have"2 dvd gcd m n"by (rule gcd_greatest)with lowest_termshave"2 dvd 1"by simpthus Falseusing odd_oneby blastqed

Isabelle has been used to aidformal methods for the specification, development andverification of software and hardware systems.

Isabelle has been used to formalize numerous theorems frommathematics andcomputer science, likeGödel's completeness theorem, Gödel's theorem about the consistency of theaxiom of choice, theprime number theorem, correctness ofsecurity protocols, and properties ofprogramming 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.^[8]

• In 2009, the L4.verified project atNICTA produced the first formal proof of functional correctness of a general-purpose operating system kernel:^[9] the seL4 (secure embeddedL4)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 languageLightweight Java was proventype-sound in Isabelle.^[10]

Several languages and systems provide similar functions:

• Agda, written inHaskell
• Rocq (previously known asCoq), written inOCaml
• Lean, written inLean itself andC++
• LEGO, written inStandard ML of New Jersey
• Mizar system, written inFree Pascal
• Metamath, written inANSI C
• Prover9, written inC, with a GUI written inPython
• Twelf, written inStandard ML

• Official website
• Isabelle on Stack Overflow
• The Archive of Formal Proofs
• IsarMathLib

• Proof assistants
• Free theorem provers
• Software using the BSD license

• Articles with short description
• Short description matches Wikidata
• Official website different in Wikidata and Wikipedia