Introduction to Formal Verification

In a world where software controls everything from pacemakers to autonomous vehicles, "it works on my machine" is no longer a sufficient guarantee. Bugs can be catastrophic. Formal methods offer a rigorous alternative: mathematically proving that software behaves appropriately according to its specification.

The Limits of Testing

Edsger W. Dijkstra famously said:

"Testing shows the presence, not the absence of bugs."

No matter how many unit tests you write, you cannot exhaustively test every possible input for a complex system. Proofs, however, cover all possible executions.

What is Formal Proof?

At its core, formal logic transforms code into mathematical objects. Just as we can prove $a^2 + b^2 = c^2$ for a right triangle, we can prove properties about programs.

Example: The Maximum Function

Consider a simple function max(a, b):

let max a b = if a >= b then a else b

Use Coq to prove its property $\forall a, b \in \mathbb{Z}, \max(a, b) \ge a$ :

Theorem max_ge_left : forall a b : Z, max a b >= a.
Proof.
  intros a b.
  unfold max.
  destruct (Z_ge_dec a b); lia.
Qed.

This isn't just a check for some random inputs, but a mathematical proof that holds for every integer in existence.

The Landscape of Formal Methods

Formal methods aren't monolithic. They span a spectrum of rigor and automation:

Domain	Application	Tool/Language
Aerospace	Flight control systems	SPARK/Ada
Finance	Smart contracts	Solidity + Certora
Security	Cryptographic protocols	ProVerif
Hardware	CPU design verification	HOL, ACL2
OS Kernels	seL4 microkernel	Isabelle/HOL

Visualizing the Process

Here is how the flow typically works, from specification to proof:

Dependent Types: Proofs as Code

Modern languages like Idris, Agda, and Lean allow you to embed proofs directly into your types.

For example, a vector Vect n a includes its length n in its type. Concatenating a vector of length $n$ and $m$ must produce a vector of length $n + m$ .

\text{Vect } n \ a \rightarrow \text{Vect } m \ a \rightarrow \text{Vect } (n + m) \ a

If the implementation returns a vector of length $n+m-1$ , the code literally will not compile.

Getting Involved

Formal logic is one of the most exciting frontiers in computer science. If you're interested in building software that cannot crash:

Learn Coq or Lean: The interactive proof assistants of choice.
Explore PRISM: We have an active research group.
Join the PRISM Systems Computing domain to start your journey.