PV6 Isabelle/HOLinteractive theorem prover

Application domain/field

Type of tool

Interactive theorem prover/proof assistant

Expected input

A 'theory' that you want to proof correct. A theory is a collection of types, functions and theorems.


HOL (for the formula that should be proven) and Isar (language for writing proof scripts).

Expected output

Whether the mathematical formula has been proven. It is also possible to turn (verified) executable specifications into code (SML, OCaml, Haskell or Scala).


This is an interactive theorem prover based on higher-order logic. It is sometimes also called a "proof assistant". You can use it to prove the correctness of mathematical formulas. E.g. you can use it to verify the correctness of a protocol. Note that proving the correctness of something is an interactive process, while the tool can deduce some things automatically, it will often require user interaction! This interaction is done through writing proof scripts in the Isar language. Isabelle is also capable of turning executable specifications directly into code in SML, OCaml, Haskell and Scala.


Related papers

Last publication date

2014 (note this is for papers about Isabelle, there are a lot of papers that use it that have been published later)

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.