formal verification

Mathematical proof that a system (software, hardware, protocol) meets its specification. Certainty beyond testing.

approaches

• model checking: exhaustive exploration of all reachable states, temporal logic (CTL, LTL), counterexample generation
• theorem proving: interactive or automated construction of proofs. Coq, Isabelle, Lean, Agda
• abstract interpretation: sound approximation of program behavior, static analysis
• SMT solvers: satisfiability modulo theories, automated decision procedures (Z3)

connection to type theory

The Curry-Howard correspondence in type theory equates proofs with programs and propositions with types. Dependently typed languages (Idris, Agda) merge programming and proving into one activity.

applications

• verified compilers: CompCert (verified C compiler)
• verified operating systems: seL4 (formally proven microkernel)
• verified consensus algorithms: proofs of safety and liveness for BFT protocols
• smart contract verification: proving correctness of on-chain logic in cyber
• hardware verification: proving chip designs match specification

relation to complexity

Verification itself can be computationally expensive. Many verification problems are undecidable in general (complexity theory), but tractable for restricted domains.