形式手法（けいしきしゅほう、英: formal methods）は、ソフトウェア工学における数学を基盤としたソフトウェアおよびハードウェアシステムの仕様記述、開発、検証の技術である[1]。ソフトウェアおよびハードウェア設計への形式手法の適用は、他の工学分野と同様、適切な数学的解析を行うことで設計の信頼性と頑健性が向上するという予想によって動機付けられている[2]。

形式手法は理論計算機科学の様々な成果を基盤として応用したものであり、数理論理学、形式言語、オートマタ理論、プログラム意味論、型システム、代数的データ型などを活用して、ソフトウェアおよびハードウェアの仕様記述とその検証を行う[3]。
分類

形式手法はいくつかの水準で使用可能である:
水準0
形式仕様記述を行い、プログラム自体を非形式主義的に行う。「軽い形式手法」と呼ぶ。費用対効果が早く得ることができる選択である。
水準1
形式手法を使って開発と検証を行い、より形式主義的にプログラムを生成する。例えば、仕様記述からのプログラム作成において詳細化と属性の証明を行う。高信頼システムに適した選択である。
水準2
自動定理証明によって完全に機械的な証明を行う。道具を整備するのに費用がかかるか、厳密である必要がありシステムを記述するのに手間がかかる。間違いが混入することで生じる損失に見合わなければ実施しない（例えば、マイクロプロセッサ設計の重要な部分など）。

詳しくは後述する。

プログラム意味論の分類に対応して、形式手法は以下のように大別する:
表示的意味論
表示的意味論では、システムの意味は領域理論で表現する。この場合、領域理論の性質によってシステムの意味を与える。しかし、あらゆるシステムが関数に直感的に表現できるわけではないとも言われている。
操作的意味論
操作的意味論では、より単純な計算モデルの一連の動作によってシステムの意味を表現する。この場合、モデルの単純性が表現を明確にする。しかし、これは意味論的な判断の先延ばしとも言われている（つまり、使用された単純な計算モデルの意味論の定義はどうなるのか？）。
公理的意味論
公理的意味論では、システムがある処理を行う前と後の（真なる）状態によってシステムの意味を表現する。この場合、古典的論理学と関係が深い。しかし、単に実行前と実行後の状態を示しただけで実際にシステムが何をするかを表現したことになるのかとの疑念も言われている。
軽量(light weight)形式手法

実際の開発に携わる人々の中には、形式手法コミュニティが仕様記述と設計の完全な形式化を強調しすぎていると感じている[4][5]。彼らは対象となるシステム自体の複雑性だけでなく使用する言語の表現能力が完全かどうかが形式化を困難にしていると主張する。代替案として様々な軽量（ライトウェイト）な形式手法が提案されてきた。それらは部分的な仕様記述と応用に注力したものである。このようなライトウェイトな形式手法の例として、型システム、uppaal Alloy オブジェクトモデリング記法[6]、Z言語によるユースケース駆動型開発[7]、CSK VDM ツールセット[8]がある。
利用

形式手法は開発工程の様々な部分に適用可能である。
仕様記述

形式手法は開発対象システムの任意のレベルの仕様を記述するのに利用可能である。そのような形式的記述はその後の開発活動のガイドとなるだけでなく、開発されたシステムの機能が要求通りであるか正確性と完全性の観点での検証にも利用可能である。

従来から、形式仕様記述システムの必要性は注目されている。ALGOL 58の報告書[9]の中でジョン・バッカスはプログラミング言語の文法の形式的記法（後にバッカス・ナウア記法、BNF記法と呼ばれるようになった[10]）を提案した。バッカスはプログラミング言語の意味論の記法の必要性にも言及した。報告書にはBNF記法と同様の意味論に関する記法を将来提案すると書かれているが、それが現われることはなかった。
開発

形式仕様記述ができると、それに従って設計を行い、実際の開発を行う（すなわち、ソフトウェアやハードウェアに実体化させる）。例えば:

操作的意味論に基づく形式仕様記述の場合、実際のシステムの動作と仕様上の動作（それ自体が実行可能/シミュレート可能）を比較する。さらにツールによってはそのような仕様記述から自動的にコードを生成するものもある。

公理的意味論に基づく形式仕様記述の場合、仕様に記された事前状態と事後状態が実行コード内にアサーションとして組み込まれる。

検証

形式仕様記述ができると、それを証明の根拠として使用することもある。
人間による証明