⭐️形式手法

設計を数式で書き、ツールで「ありうる全パターン」を調べて、ルールが破れないことを確かめる手法。

• テスト: 試したケースだけ確認できる
• 形式手法: 全パターンを確認できる。破れるなら、破れる手順を具体的に出してくれる

並行処理や分散システムのように、タイミング次第でまれにしか起きないバグを探すのに向く。代表的なツールは TLA+。