システムの仕様や設計が正しいことを、数学的な手法を用いて厳密に証明する技術を何というか。

モデル検査や定理証明を用いて、バグや論理的誤りがないかを網羅的に確認する。