形式手法が適しているもの
抽象的なライブラリのコードの検証
仕様バグの検出
デッドロックやデータレース、レースコンディション等、確率的に発生する不具合の防止
分散処理、分散アルゴリズム、スマートコントラクト
モジュールを結合した時の不整合の検出