形式検証 (Formal Verification)

仕様を形式言語で表し、モデル検査・定理証明・型検査などで、実装がその性質を満たすかを機械的に確かめる手法。テストが選んだ実行例を調べるのに対し、形式検証は明示したモデルと性質の範囲全体を対象にする。

まず安全性・到達可能性・不変条件など、検証したい性質と対象モデルを小さく定める。次に反例を読んで仕様の誤りと実装の誤りを分離し、証明の前提・抽象化・環境仮定を記録する。

検証済みでも仕様が間違っていれば価値はない。状態空間の爆発、外部環境のモデル化、証明器の前提、運用時の設定変更が保証の境界になる。