このページでは，形式手法における検証という側面について解説します．形式手法においては，理論に基づいた科学的・系統的な検証，特に網羅的な検証を考えます．検証のアプローチは二つ考えられます．一つは「実行・観測」に基づいた検証であり，テストやシミュレーション，特に網羅的な検査（モデル検査）などを考えて性質が成り立つかどうかを調べるものです．もう一つは「法則・説明」に基づいた検証であり，理論的に性質が成り立つことを示していくもの（定理証明）です．
何かしらの記述を行った際に文法チェックなど基本的なチェックを行うことは当然として，多くの形式手法では「ある性質が成り立つか成り立たないか」ということの検証手段（理論基盤とツール）を提供しています．検証対象となる性質としては，「デッドロックしない」といったアプリケーション非依存の性質もあれば，要求から導かれるアプリケーション依存の性質もあります．いずれにしても，「正しい」「誤りがある」という判断は，ある基準（性質が成り立つかどうか）に対する相対的なものとなります．
検証の対象となる性質
本サイトでは形式手法の代表例として，SPINの例，VDMの例を挙げてきました．SPINの場合，検証の対象となる性質は「実行の経過」に関するものです．例えば以下のような性質になります．
VDMの場合，検証の対象となる性質は「システムの状態と計算・操作」に関するものです．例えば以下のような性質になります．
形式手法における検証の方法には大きく分けて二つのアプローチがあります．一つは「実行・観測」に基づいた検証，特にモデル検査，もう一つは「説明」に基づいた検証，定理証明です．以下ではこれらのアプローチそれぞれについて説明します．
「動かしてみて観測する」ことによる検証
性質が成り立つかどうかを調べる一つの手段は，実際にシステムのモデル上においてその動作を考えてみて，どう実行が進んでいくのか試してみることです．例えば試すべき状況（テストケース）を設定して，シミュレーション・実行を行ってみること（テスティング）が考えられます．形式手法の場合特に，「どういう状況を期待しているのか」「どういう状況が望ましくないのか」という検証対象となる性質を明確にし，様々な実行の状況においてそれが成り立つかどうかを観測します．また多くの場合，プログラムそのものではなく，より抽象的な，詳細を省いたモデルを対象とすることにより，開発の早い段階でシステムの重要な部分・側面に焦点を絞って検証を行うことを考えます．
ただし，一般的なシステムでは様々な要因によって実行の順序や分岐が変化し，特定の状況においてのみ誤りが発生・顕在化します．例えば，特定のデータが入力された際のみうまく処理されず望ましくない状態になってしまう場合や，複数の並行プロセスが特定の実行順序のときのみデッドロックする場合などがよくあります．一般的なテスティングによる検証手法では，網羅的にそういった状況を調べるのは困難であり，「テスト漏れ」の不安がつきまとうところがあります．
モデル検査と呼ばれる検証方式においては，ツールに可能な状態遷移を網羅的に調べさせることにより，性質が成り立つかどうかを検証します．「すべての可能性を調べたが，問題となる状況がなかった」「すべての可能性を調べたら，問題のある状況があった」ということをツールに報告させるわけです．
ただ「すべての可能性を調べる」というだけでは，「非現実的，無理だ」ということになってきます．例えばプログラムにおいて，整数型の変数の値をすべて（2の32乗通り）試してみるようなことは非現実的です．モデル検査においては，データの詳細などは捨象し，「実行の順序や分岐がどう変わる可能性があるか」という部分に限定した抽象的なモデルを用い，そのモデル上で網羅的な検査を行います．また，実際に「網羅的に実行してみる」というよりは，「網羅的に実行してみるのと理論的に同等の検査」を正しく，効率よく行う手段を提供しています．
「法則を説明する」ことによる検証
性質が成り立つかどうかを調べる一つの手段は，性質が成り立つことを理論的に説明することです．例えば，以下の状況を考えてみます．
この場合，「正の数と正の数を足した結果は正である」という数の性質を用いて「戻り値が必ず正となる」ことを説明できます．「実行・観測」によるアプローチの場合，「引数が3と5の場合」「引数が10と12の場合」といった様々な具体的な状況を試してみるわけですが，「説明」によるアプローチでは，上記のように一般化した理屈で性質が成り立つことを説明していきます．
上記は直感的な説明ですが，何となく「成り立ちそう」と思うだけでは確信が持てません．このため，形式手法では特に数学的な考え方に基づいた厳密な証明を考えます．不等式（より小さい）や全称記号（xがどの値をとっても）といった厳密な数学的記法を用い，必要ならば帰納法や背理法といった証明手法を用いていくこととなります．
その際のツールによる支援としては，証明すべき命題の洗い出しとそれらの自動証明が主となります．システム内の様々な変数やそれに対する操作を考えたとき，上記のように証明が簡単な性質も多く出てきます．そういった部分に対してはツールに自動証明を行わせることができるようになっています．ただし，「どんな場合でも完全な自動証明を行う」ことはできないので，ツールが詰まった場合には，場合分けや定理の適用を指示するなど人間が手助けする必要があります．
ライトウェイトな検証手法
誤りが人命に関わるような交通システム，誤りが高コストの「回収」につながるようなハードウェアなどにおいては，モデル検査または定理証明を用いることが一般的になってきています．むしろ，認証の要件になるなど必須にもなってきています．これは，これらの手法が科学的，かつ網羅的・系統的な検証手段を提供しているためです．
しかし，モデル検査や定理証明など，（少なくとも現在一般的な）プログラマが手慣れていない検証手法を用いることは負担が大きい場合もあります．多くのシステムにおいては，「一般的な状況における動作をある程度検証できたらタイムリーにリリースすることを重視し，誤りが見つかったらアップデートを適切に発行すればよい」という考え方で十分かもしれません．そのような場合に形式手法を活用する方法として，開発の早い段階で抽象的なモデル上での手軽なテスティング・プロトタイピングを行い，誤りや曖昧さなどを「早めにできるだけ」排除することが考えられます．VDMなどはこの思想に基づいており，しばしば「ライトウェイトな形式手法」と呼ばれます．