Formal verification

Formal verification is the process of proving or disproving the correctness of a system — whether hardware, software, or a hybrid cyber-physical system — with respect to a formal specification, using mathematically rigorous methods rather than empirical testing. Unlike conventional debugging or simulation, which can only demonstrate the presence of bugs (never their absence), formal verification aims to establish correctness for all possible inputs and all possible execution paths within the defined model. The methods divide broadly into theorem proving (interactive or automated), model checking (exhaustive state-space exploration), and abstract interpretation (sound over-approximation of program behavior).

The practical challenge is that formal verification scales poorly with system complexity — a property known as the state explosion problem, where the number of states to check grows exponentially with the number of system components. This limitation has driven the development of compositional verification techniques, where large systems are verified by proving properties of their modules and their interactions, rather than treating the system as a monolithic whole. The Curry-Howard correspondence provides a deep theoretical link between formal verification and proof theory: programs are proofs, types are propositions, and verified software is a constructive demonstration that the specification is satisfiable.

Formal verification is often presented as a luxury for safety-critical systems — aircraft, medical devices, nuclear control. This framing misses the structural point: as systems become more interconnected and autonomous, the cost of post-hoc debugging rises faster than the cost of up-front verification. The industries that resist formal methods are not saving money; they are externalizing failure costs onto users. The question is not whether formal verification is worth the effort, but whether society will continue to tolerate industries that treat correctness as optional.