Program verification

Program verification is the application of formal methods to demonstrate that a computer program satisfies its specification. It encompasses a range of techniques — from model checking finite-state abstractions to theorem proving full functional correctness — and it stands in contrast to software testing, which can only demonstrate the presence of bugs, never their absence. Program verification aims to make software correctness a matter of mathematical demonstration rather than empirical confidence.

The field has produced landmark achievements: the verified operating system kernel seL4, the verified C compiler CompCert, and components of the Microsoft Hyper-V verified using VCC. Yet program verification remains a specialized discipline. The labor required to verify even modest programs is substantial, and the specifications themselves are often more complex than the code. The emerging paradigm of correctness by construction — building programs alongside their proofs, rather than verifying after the fact — and design by contract offer paths toward integration, but the gap between verified code and mainstream engineering practice remains wide.

The ultimate question for program verification is not whether it is possible. It is whether the cost of certainty is worth paying, and for which systems the answer is yes.