Test Automation

Formal Verification with Isabelle/HOL for Critical Software

HelpMeTest

HelpMeTest

— 6 min read
Formal Verification with Isabelle/HOL for Critical Software

In 2009, researchers at NICTA published a paper with an extraordinary claim: they had formally verified the functional correctness of the seL4 microkernel — 7,500 lines of C code — proving mathematically that the implementation matches its specification for every possible input and execution path. This was not testing. It was not model checking within bounds. It was a machine-checked mathematical proof. The tool they used was Isabelle/HOL.

Isabelle/HOL represents the upper end of the verification spectrum. It requires more expertise than model checking, takes more time, and is suited for smaller codebases and critical components. But when you need a guarantee that no testing methodology can provide — that the code is correct for all inputs, not just the ones you tested — theorem proving is the only answer.

Theorem Proving vs Model Checking

The distinction is fundamental:

Model checking is automatic and exhaustive within a finite bound. You describe your system, specify a property, and the model checker explores all states within the given scope. It either finds a counterexample or confirms the property holds for all states up to that scope. TLA+ and SPIN are model checkers.

Theorem proving is interactive (semi-automated). You write a formal proof that a property holds for all inputs, for all possible executions, without any finite bound. The proof assistant verifies each step of your reasoning. You guide the proof; the system checks it.

Model checking is more accessible and sufficient for most protocol and design verification. Theorem proving is harder but gives absolute guarantees. The two are complementary: use model checking to find bugs early, use theorem proving for the most critical components when you need mathematical certainty.

What Isabelle/HOL Is

Isabelle is a proof assistant developed at Cambridge and Munich. The /HOL suffix refers to Higher-Order Logic, the logical foundation it uses. HOL supports:

  • Types (polymorphic, recursive)
  • Functions (total, partial, recursive)
  • Sets and relations
  • Mathematical induction
  • Classical and intuitionistic reasoning

Isabelle/HOL is not a programming language, though you can define executable functions in it. It is a language for writing mathematical theorems and proofs. The Isabelle system checks your proof mechanically — it cannot be fooled by a plausible-but-wrong argument.

Other theorem provers you may encounter: Coq (used to prove the Four Color Theorem and verify CompCert, a verified C compiler), Lean (increasingly popular for mathematics), ACL2 (used extensively at Intel for hardware verification), and PVS (widely used in aerospace).

Installing Isabelle

Download Isabelle from isabelle.in.tum.de. The download is a self-contained bundle. The primary interface is the Isabelle/jEdit IDE, which provides real-time proof checking — as you type, Isabelle checks your work and highlights errors.

# On macOS, download the .dmg and install
<span class="hljs-comment"># Then run from the command line:
/Applications/Isabelle2024.app/Isabelle/bin/isabelle jedit

Basic Isabelle/HOL Concepts

A theory file (.thy) contains definitions, lemmas, and proofs:

theory FirstProof
  imports Main
begin

(* A simple function *)
fun factorial :: "nat ⇒ nat" where
  "factorial 0 = 1"
| "factorial (Suc n) = Suc n * factorial n"

(* A property we want to prove *)
lemma factorial_positive: "factorial n > 0"
  by (induct n) simp_all

(* A more complex property *)
lemma factorial_mono: "n ≤ m ⟹ factorial n ≤ factorial m"
  apply (induct m)
  apply simp
  apply (case_tac "n = Suc m")
  apply simp
  apply (simp add: le_Suc_eq)
  done

end

The by simp_all tactic asks Isabelle to discharge the proof automatically using its simplifier. The apply form is step-by-step. The lemma factorial_positive says: for all natural numbers n, factorial n > 0. The proof is by induction: the base case (n=0) gives factorial 0 = 1 > 0, and the inductive step follows from the inductive hypothesis.

Proving Algorithm Correctness

A more realistic example: proving that a sorting algorithm actually sorts. Here we verify insertion sort:

theory InsertionSort
  imports Main "HOL-Library.Multiset"
begin

fun insert :: "'a::linorder ⇒ 'a list ⇒ 'a list" where
  "insert x [] = [x]"
| "insert x (y#ys) = (if x ≤ y then x#y#ys else y # insert x ys)"

fun isort :: "'a::linorder list ⇒ 'a list" where
  "isort [] = []"
| "isort (x#xs) = insert x (isort xs)"

(* Sorted predicate *)
fun sorted :: "'a::linorder list ⇒ bool" where
  "sorted [] = True"
| "sorted [x] = True"
| "sorted (x#y#ys) = (x ≤ y ∧ sorted (y#ys))"

(* Insertion preserves sortedness *)
lemma insert_sorted: "sorted xs ⟹ sorted (insert x xs)"
  apply (induct xs)
  apply simp
  apply (auto simp add: sorted.simps split: if_splits)
  done

(* isort produces a sorted list *)
theorem isort_sorted: "sorted (isort xs)"
  apply (induct xs)
  apply simp
  apply (simp add: insert_sorted)
  done

(* isort preserves the multiset of elements *)
lemma insert_multiset: "mset (insert x xs) = {#x#} + mset xs"
  apply (induct xs)
  apply simp
  apply (auto split: if_splits)
  done

theorem isort_permutation: "mset (isort xs) = mset xs"
  apply (induct xs)
  apply simp
  apply (simp add: insert_multiset)
  done

end

isort_sorted proves the output is sorted. isort_permutation proves it contains exactly the same elements as the input (it has not dropped or duplicated anything). Together, these two theorems prove insertion sort is correct — not for specific inputs, but for all possible inputs of any length.

The seL4 Verification

The seL4 verification is worth examining because it demonstrates what Isabelle/HOL can achieve at industrial scale.

seL4 is a microkernel — the most privileged software on a computer, running below the OS. A bug in the kernel can compromise the entire system. The verification established:

  1. Functional correctness: The C implementation refines the abstract specification. Every system call, every state transition, every memory access in the C code matches the corresponding operation in the formal spec.
  2. Integrity: Untrusted code cannot modify trusted data. Formally proved, not just tested.
  3. Confidentiality: Untrusted code cannot read trusted data.

The verification involved approximately 200,000 lines of Isabelle proof script for 7,500 lines of C. The proofs took a team of researchers several years to complete. But once done, they provide guarantees no testing campaign can match.

The key technique is refinement: you have an abstract model (mathematically clear but not executable), a concrete model (more detailed), and the C implementation. You prove that each level correctly implements the one above it. Errors at the C level that don't affect observable behavior are fine. Errors that deviate from the spec cause proof failures.

Formal Verification in Aerospace and Finance

Formal verification has a long history in safety-critical domains:

Aerospace: NASA has used PVS (a Coq-family prover) to verify guidance systems. The Airbus A380 fly-by-wire software was developed with formal methods tools. DO-178C, the certification standard for avionics software, now explicitly recognizes formal methods as a means of compliance.

Finance: J.P. Morgan and other firms have used formal verification for trading algorithms and settlement logic where a subtle overflow or rounding error can cost millions. The Ethereum blockchain was verified using the K framework (a rewriting-logic-based verifier).

Cryptography: Many cryptographic protocol implementations have been formally verified. The HACL* library provides formally verified implementations of SHA-2, Curve25519, and other algorithms, and it is used in Firefox and Signal.

When to Use Theorem Proving vs Testing

Theorem proving is not a replacement for testing in general software development. The cost-benefit ratio favors theorem proving only in specific situations:

Use theorem proving when:

  • The cost of a bug is catastrophic (safety of life, large financial loss, security breach)
  • The component is small but critical (a kernel, a cryptographic primitive, a scheduling algorithm)
  • The property needs to hold for all inputs without exception
  • You have the resources and expertise

Use testing when:

  • The codebase is large and complex
  • Behavior depends on integration with external systems
  • The failure cost is tolerable and bugs can be fixed in production
  • Time-to-market is a constraint

Use model checking when:

  • The system is concurrent or distributed
  • Protocol correctness needs to be verified
  • You need exhaustive checking within a finite scope
  • You want to find bugs quickly before writing code

For most software teams, the practical path to formal methods starts with property-based testing (QuickCheck, Hypothesis), then model checking for critical protocols (TLA+, SPIN), and theorem proving only for the absolute core that must be provably correct.

Getting Started

The Isabelle tutorial on the official site is thorough. The book "Concrete Semantics" by Nipkow and Klein (available free as a PDF) teaches Isabelle through programming language semantics and is the best introduction for software engineers.

The Archive of Formal Proofs (AFP) at isa-afp.org contains thousands of verified theories covering algorithms, data structures, protocols, and mathematics. Before writing a proof from scratch, check whether someone has already proved what you need.

The investment in learning Isabelle/HOL is significant, but for teams building safety-critical software, it pays back quickly. A formally verified component does not have bugs in the verified properties. That is a guarantee worth having.

Read more