TL;DR
ソフトウェアやシステムの設計・開発・分析に、形式的（数学的・論理的）な記述やモデルを使うアプローチ全般を指す。
なぜ必要か
形式手法は、設計から仕様化、検証、テストまで、ソフトウェア開発のライフサイクル全体で使われる。生成 AI との相性も良いとされる（AIと共に進化する開発手法：形式手法と関数型プログラミングの可能性）。
Wikipedia の「形式手法」によると、適切な数学的解析をすれば設計の信頼性と頑健性が高まる、という考えが動機になっている。航空宇宙工学のように、誤りが人命に関わる分野で広く使われている。
仕組み
自動で証明する手法には、大きく次の 2 つがある。
例
代表的なツールや技法には次のものがある。
- Alloy: 関係モデルを使ってシステムを設計・分析するためのツール
- TLA+: 時相論理をベースにした、システムの設計と検証のためのフレームワーク
- Z 言語: ソフトウェアの仕様を書くための形式的な仕様記述言語
- B メソッド: システムの仕様から正しい実装を導く方法論
注意点
Wikipedia によると、人手による証明も自動証明も時間と費用がかかるので、利益が費用を上回る場合や、誤りによる損害が大きい場合にしか使われない。モデル検査は、適切に抽象化したモデルがないと状態の数が膨大になる。完全な形式化は難しいので、仕様の一部だけを形式的に書く軽量な形式手法も提案されている。