ソフトウェアやハードウェアの設計が仕様通りであることを、数学的な論理モデルを用いて網羅的に証明する手法はどれか。

全ての入力パターンに対してバグがないことを論理的に保証する極めて厳密な検証手法である。