形式検証
プログラムが仕様を満たすことの数学的な証明。テストはバグの存在を示せるが、形式検証はその不在を示せる。
証明支援系には、Coq（現 Rocq、1989年頃、フランス）、Agda、Lean（Microsoft Research発。2024年の数学証明の変革を牽引した）、Isabelle/HOL などがある。検証済みシステムの有名な例は、seL4（カーネル、2009年。古典的なカーネルのバグ類型を長いリストにわたって含まないと証明された）、CompCert（正しさが証明されたCコンパイラ）、Project Everest（検証済みTLS）。
学習曲線は急で、単純なプログラムの検証にも数か月から数年かかる。航空、原子力、暗号ライブラリのように、安全性が極めて重要なコードにだけ見合う投資だ。