Formal verification: checking every case, not just some
Tests try some inputs and hope the rest behave. Formal verification uses math and clever search to check all of them. In this lesson you catch a bug that tests miss, write a precise description of what code should do, let a computer explore every state of a small program, and prove a loop correct.
Formal verification shows that a system meets a specification for every input or every reachable state, either by exhaustive search (model checking, SMT) or by deductive proof (Hoare logic, proof assistants). The guarantee is exactly as strong as the specification and the assumptions behind it.
Why tests aren't enough
This abs function should never return a negative number. It works on small 8-bit whole numbers, from −128 to 127. That is only 256 possible inputs. Run 100 random tests, then check every input.
The same abs, now on 16-bit two's complement integers: 65,536 inputs and exactly one counterexample. Compare random testing with an exhaustive check, then see why exhaustive checking stops scaling and what SMT solvers do instead.
// 8-bit signed integer: -128 … 127
function abs(x) {
if (x < 0) return -x;
return x;
}
// Promise: abs(x) >= 0 for every x
#include <stdint.h>
int16_t abs16(int16_t x) {
return x < 0 ? (int16_t)-x : x;
}
// Property: for all x, abs16(x) >= 0
-(-128) does not fit and wraps around to −128 again. Only 1 input in 256 shows the bug, so random tests usually miss it. Checking every input finds it every time. Real programs have far too many inputs to try one by one, which is why verification tools reason about all inputs at once.
Exhaustive checking does not scale
Time to try every input at one billion checks per second:
| Inputs | Count | Time |
|---|---|---|
| one int8 | 256 | under 1 µs |
| one int16 | 65,536 | about 66 µs |
| one int32 | 4.3 × 10⁹ | about 4.3 s |
| one int64 | 1.8 × 10¹⁹ | about 585 years |
| two int64 | 3.4 × 10³⁸ | about 10²² years |
(declare-const x (_ BitVec 32)) (define-fun abs32 ((v (_ BitVec 32))) (_ BitVec 32) (ite (bvslt v #x00000000) (bvneg v) v)) (assert (bvslt (abs32 x) #x00000000)) (check-sat) ; sat (get-model) ; x = #x80000000 (-2147483648)
- sat with a model: a concrete counterexample, here
x = INT_MIN. - unsat: no input violates the property. That is a proof over all 2³² inputs. Add the precondition
x != INT_MINand the query becomes unsat.
-x on INT_MIN for 32-bit int is undefined behaviour, which is worse than a wrong answer. The same family of bugs hid for years in (low + high) / 2 inside binary search in the Java standard library, until arrays grew past 2³⁰ elements.
Specifications: saying exactly what "correct" means
To check a program, you first have to write down what it should do. This is the specification, or spec. Here the job is to sort a list of numbers. Tick the rules you want to require. The checker tries every short list and shows which of the four programs still pass.
A specification is a set of postconditions (and preconditions) over inputs and outputs. Build the spec for Sort clause by clause. A bounded checker runs each implementation on every list of length 0 to 4 over {0, 1, 2} (121 inputs) and reports the first counterexample per clause set.
- A precondition is what must be true before the code runs. Example: "the list is not empty" before taking its first item.
- A postcondition is what the code promises when it finishes. Example: "the result is sorted".
- An invariant is something that stays true the whole time. Example: "the account balance is never negative".
method BinarySearch(a: seq<int>, key: int) returns (i: int) requires forall p, q :: 0 <= p < q < |a| ==> a[p] <= a[q] ensures 0 <= i ==> i < |a| && a[i] == key ensures i < 0 ==> key !in a
requiresis an obligation on every caller. Inside the method it is an assumption.ensuresis an obligation on the method body, and callers may rely on it.- Class or loop invariants must hold at stated points (method entry and exit, each loop iteration).
- Bounded checks like the one above are not proofs. They rely on the small scope hypothesis: most bugs show up on small inputs. A verifier like Dafny proves the clauses for lists of any length.
Model checking: explore every state
Two programs share one printer. Only one may print at a time: that part of the code is the critical section. Each program has a flag it raises to say "I want in". A model checker tries every possible order in which the two programs can take their steps, and looks for a bad state.
Two processes, shared flags, and a mutual exclusion property. The checker runs a breadth-first search over the interleaving semantics: a state is (pc₀, pc₁, flag₀, flag₁, turn), and each transition is one atomic step of one process. It checks the invariant on every reachable state and looks for deadlocks.
State explosion
Each process here has 4 locations. Before counting shared variables, N processes give up to 4N combinations:
| Processes | Location combinations |
|---|---|
| 2 | 16 |
| 4 | 256 |
| 8 | 65,536 |
| 16 | 4.3 × 10⁹ |
| 32 | 1.8 × 10¹⁹ |
Real checkers fight this with partial-order reduction (skip orderings of independent steps), symmetry reduction, symbolic representations (BDDs), and bounded model checking with SAT/SMT, which checks all runs up to k steps.
Safety vs. liveness
- Safety: nothing bad ever happens. "Never both in the critical section." A violation is a finite trace to a bad state.
- Liveness: something good eventually happens. "A process that wants in eventually gets in." A violation is an infinite run, shown as a lasso: a path into a cycle that never reaches the good state. Checking it needs fairness assumptions, or a scheduler that never runs one process could "starve" anyone.
- The "flags first" protocol is safe, but it can deadlock: both flags up, both waiting forever. Freedom from deadlock is necessary for liveness but not enough. Peterson's algorithm also guarantees no starvation under weak fairness.
---- MODULE Peterson ----
VARIABLES pc, flag, turn
vars == <<pc, flag, turn>>
Other(i) == 1 - i
Init == /\ pc = [i \in {0, 1} |-> "idle"]
/\ flag = [i \in {0, 1} |-> FALSE]
/\ turn = 0
Raise(i) == /\ pc[i] = "idle"
/\ flag' = [flag EXCEPT ![i] = TRUE]
/\ pc' = [pc EXCEPT ![i] = "turn"]
/\ UNCHANGED turn
Yield(i) == /\ pc[i] = "turn"
/\ turn' = Other(i)
/\ pc' = [pc EXCEPT ![i] = "wait"]
/\ UNCHANGED flag
Enter(i) == /\ pc[i] = "wait"
/\ (~flag[Other(i)] \/ turn = i)
/\ pc' = [pc EXCEPT ![i] = "crit"]
/\ UNCHANGED <<flag, turn>>
Leave(i) == /\ pc[i] = "crit"
/\ flag' = [flag EXCEPT ![i] = FALSE]
/\ pc' = [pc EXCEPT ![i] = "idle"]
/\ UNCHANGED turn
Proc(i) == Yield(i) \/ Enter(i) \/ Leave(i)
Next == \E i \in {0, 1} : Raise(i) \/ Proc(i)
Spec == Init /\ [][Next]_vars
/\ \A i \in {0, 1} : WF_vars(Proc(i))
MutualExclusion == \* safety
~(pc[0] = "crit" /\ pc[1] = "crit")
NoStarvation == \* liveness
\A i \in {0, 1} : pc[i] = "turn" ~> pc[i] = "crit"
====
Proving a loop correct
A model checker needs a small, finite world. To prove code correct for any input, we reason instead. Loops are the hard part. The trick is a loop invariant: a fact that is true every time the loop is about to check its condition. Run the loop below, then pick the invariant that proves it adds up the list correctly.
Hoare logic proves triples {P} S {Q}. For a loop, you supply an invariant I and discharge three verification conditions, plus a variant for termination. Run integer division by repeated subtraction, then choose I and a variant. Each obligation is checked over every state with n ≤ 12, d ≤ 4 and small q, r; a verifier like Dafny would prove them for all integers with an SMT solver.
Which invariant proves it?
Termination: pick a variant
Partial correctness says "if the loop stops, the result is right". For total correctness, give an integer expression that is never negative while the loop runs and gets strictly smaller on every iteration. It cannot shrink forever, so the loop must stop.
- Is it true at the start, before the first iteration?
- If it is true before an iteration, is it still true after that iteration?
- When the loop stops, does the invariant plus "the condition is now false" give the answer we promised?
- Initiation: {P} init {I}. The precondition and the initial assignments establish I.
- Preservation: {I ∧ B} body {I}. One iteration from any state satisfying I and the guard B ends in I.
- Exit: I ∧ ¬B ⇒ Q. Together with the negated guard, I implies the postcondition.
- Termination: I ∧ B ⇒ V ≥ 0, and {I ∧ B ∧ V = V₀} body {V < V₀}.
q * d <= n fails: it does not say enough to carry itself through one step. Strengthening the invariant is the everyday work of proof.
Where the tools fit
In the real world
- seL4: a microkernel whose C code is proved in Isabelle/HOL to implement its abstract specification, with proofs of security properties on top. The proof assumes a correct compiler, boot code and hardware; later work checks the compiled binary too.
- CompCert: a C compiler proved in Coq to preserve the meaning of the programs it compiles. When researchers threw millions of random programs at many compilers, they found no wrong-code bugs in CompCert's verified parts, only in the unverified front end.
- AWS: engineers have used TLA+ since 2011 on systems such as S3 and DynamoDB. Model checking found subtle design bugs that needed traces of dozens of steps, which testing and review had missed.