Applications
Isabelle has been used to aid formal methods for the specification, development and verification of software and hardware systems.
- The use of Isabelle by Hewlett-Packard in the design of the HP 9000 line of servers' Runway bus, leading to the discovery of a number of bugs uncaught by previous testing and simulation.
- 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 8,700 lines of C and 600 lines of assembler. 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 160 bugs in the C code of the seL4 kernel, and about 150 issues in each of design and specification.
- The programming language Lightweight Java was proven type-sound in Isabelle.
Larry Paulson keeps a list of research projects that use Isabelle.
Read more about this topic: Isabelle (proof Assistant)