Formal Verification: Proving a Program Correct

Testing samples inputs; a proof covers all of them. Three traditions do this and each hits a different wall. Deductive proof turns a program into a relation between assertions, and stalls at the loop invariant no machine can supply. Type-level encoding makes wrong programs unwritable, and pays with a language that rejects some correct ones. Model checking searches every state exhaustively, and is bounded by how many there are. The path ends with two systems that were actually verified, and what they cost.