What is verified software?

Testing vs. proof

Testing checks that software works for specific inputs. You write a test that says add(2, 3) == 5, run it, and confirm it passes. But you haven't checked add(2147483647, 1), or any of the other billions of possible inputs. Testing shows the presence of bugs, never their absence.

Formal verification takes a different approach. Instead of checking examples, you write a mathematical statement — a theorem — that describes what the software should do for all inputs. Then a computer checks that the proof holds. If it does, you have a guarantee that covers every possible case.

Consider Heartbleed, the OpenSSL vulnerability that exposed sensitive data across the internet for over two years. The bug was a missing bounds check — the code read past the end of a buffer. Standard testing missed it because the bug only triggered under specific conditions. A formal specification of the buffer's access bounds would have made this class of bug impossible.

How formal verification works

The process has three parts:

1. Specification — You write a precise mathematical description of what the software should do. For a sorting function, the specification says: the output is a permutation of the input, and every element is less than or equal to the next.
2. Implementation — You write the actual code, often in the same language as the specification (like Lean 4) or in a target language (like C) that gets modeled formally.
3. Proof — You construct a proof that the implementation satisfies the specification. A proof assistant mechanically checks every step. No human judgment is required for the checking — either the proof is valid or it isn't.

Think of it as type systems taken to their logical extreme. A type system proves simple properties (this variable is an integer, not a string). Formal verification proves arbitrary properties (this function never returns a negative number, this protocol never deadlocks, this compiler preserves program semantics).

Two approaches

Formal verification splits into two major families:

Model checking exhaustively explores every possible state a system can reach. It's automated — you describe the system and the property, and the tool checks all states. The downside: it can only handle finite state spaces, so it works best for hardware and protocols with bounded behavior.

Theorem proving constructs a mathematical proof that a property holds for all inputs. It can handle infinite state spaces and arbitrary complexity, but it requires human guidance (or increasingly, AI guidance) to build the proof. This is the approach used by Lean, Coq, and Isabelle.

Why Lean 4 is winning: Unlike older proof assistants designed primarily for mathematicians, Lean 4 is a real programming language — you can write executable code and prove properties about it in the same file. Its Mathlib library contains over 210,000 formalized theorems, making it the largest single repository of machine-checked mathematics. Crucially, AI models like Leanstral and DeepSeek-Prover can read and write Lean, which means the cost of building proofs is dropping fast.

Key terms