形式証明とは、明確に定義された論理ルールに従って、ある命題（主張）が真であることを一歩一歩証明していく方法です。自然言語ではなく、記号と論理だけで構成された「形式的な」方法で記述されるのが特徴です。日々のプログラミングでは、テストを書いて動作を確認するのが一般的です。しかし、
次のような状況ではテストだけでは不十分になることがあります
こうした 安全性や正しさが致命的に重要なシステムでは、「テストでは見つけられなかったバグ」が命取りになりかねません。そこで登場するのが、形式証明です。
形式証明では、プログラムやアルゴリズムが「正しい」と数学的に証明することができます。つまり「絶対にバグがない」と言えるレベルまで信頼性を高められるのです。
