Formal Verification。ある性質を形式仕様に基づいて数学的に証明することを言います。検証方法によって、定理証明法とモデル検査法が知られています。検証対象となる性質は、都合の悪い状態に決して到達しないという安全性プロパティ、いつか必ず望ましい状態になるという活性プロパティ、ある状態に到達することが可能であるという到達性プロパティなど時間的な事象のことです。Ansys SCADEでは、安全性プロパティを検証対象として記述することができ、検証方法は、モデル検査によって実行されます。