Editing Isabelle (proof assistant) (section)

==Applications==
Isabelle has been used to aid [[formal methods]] for the specification, development and [[Formal verification|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 protocol]]s, and properties of [[Formal semantics of programming languages|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.<ref>{{cite web |last1=Eberl |first1=Manuel |last2=Klein |first2=Gerwin |last3=Nipkow |first3=Tobias |last4=Paulson |first4=Larry |author4-link=Lawrence Paulson |last5=Thiemann |first5=René |title=Archive of Formal Proofs |url=https://www.isa-afp.org/ |access-date=22 October 2019 |ref=AFP}}</ref>

* In 2009, the L4.verified project at [[NICTA]] produced the first formal proof of functional correctness of a general-purpose operating system kernel:<ref Name="Klein_EHACDEEKNSTW_09">
{{ cite conference
 |last1=Klein
 |first1=Gerwin
 |last2=Elphinstone
 |first2=Kevin
 |last3=Heiser
 |first3=Gernot
 |last4=Andronick
 |first4=June
 |last5=Cock
 |first5=David
 |last6=Derrin
 |first6=Philip
 |last7=Elkaduwe
 |first7=Dhammika
 |last8=Engelhardt
 |first8=Kai
 |last9=Kolanski
 |first9=Rafal
 |last10=Norrish
 |first10=Michael
 |last11=Sewell
 |first11=Thomas
 |last12=Tuch
 |first12=Harvey
 |last13=Winwood
 |first13=Simon
 |title=seL4: Formal verification of an OS kernel
 |book-title=22nd ACM Symposium on Operating System Principles
 |pages=207–200
 |date=October 2009
 |location=Big Sky, Montana, US
 |url=http://www.sigops.org/sosp/sosp09/papers/klein-sosp09.pdf
}}</ref> the seL4 (secure embedded [[L4 microkernel family|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 soundness|type-sound]] in Isabelle.<ref>{{Cite journal |last1=Strniša |first1=Rok |last2=Parkinson |first2=Matthew |date=7 February 2011 |title=Lightweight Java |url=https://www.isa-afp.org/entries/LightweightJava.html |access-date=2019-11-25 |journal=Archive of Formal Proofs |edition=February 2011 |issn=2150-914X}}</ref>