フォーマル検証（形式検証）とは、回路の正しさをシミュレーションのように入力パターンを与えて確かめるのではなく、数学的な手法で証明する検証の総称です。代表的なのが等価性検証（Equivalence Checking）で、たとえばRTL（回路の動作記述）と、それを論理合成したゲートレベルのネットリストが、あらゆる入力に対して同じ出力を返すことを網羅的に証明します。シミュレーションでは現実的な時間で全入力を試せない大規模回路でも、漏れのない確認ができるのが特長です。
等価性検証は設計フローの中で何度も使われます。（1）RTL対ゲート：論理合成ツールが最適化の過程で機能を変えていないかの確認。（2）ゲート対ゲート：スキャンチェーンの挿入、配置配線でのバッファ挿入やセルの置き換え、テープアウト直前の修正（ECO）の前後で機能が変わっていないかの確認です。代表的なツールにSynopsys Formality、Cadence Conformalがあります。
フォーマル検証にはもう一つ、プロパティ検証（モデル検査）があります。「要求を出したら必ず応答が返る」「2つの信号が同時に1にならない」といった満たすべき性質（プロパティ）を記述し、それが到達しうるすべての状態で成り立つかを証明します。反例が見つかれば、違反に至る入力の系列がそのまま示されるため、シミュレーションでは再現しにくい深いコーナーケースのバグ発見に強い手法です。Cadence JasperGoldなどが使われます。
フォーマル検証は万能ではありません。状態数が爆発的に増える大規模な回路全体を一度に証明するのは難しく、プロパティ検証はブロック単位で適用するのが一般的です。また、証明できるのは「書いた仕様どおりか」であって、仕様そのものの誤りは見つけられません。そのため実際の検証は、シミュレーション（UVMなど）・フォーマル検証・エミュレーションを組み合わせて進められます。
