TL;DR
ソフトウェアが正しく動作することを、論理的・数学的なモデルを使って証明する手法である。プログラムが特定の仕様（要件）を満たしていることを、手動またはツールで証明する。
なぜ必要か
テストは、用意した入力に対して期待どおりに動くかを確かめるものである。形式的検証はそれと違い、ロジックを解析して正しさを確かめる。そのため、テストで試していない入力についても正しさを示せる。
仕組み
Wikipedia の「形式的検証」によると、検証は実際のシステムを抽象化した数理モデルの上で行い、手法は大きく 2 つある。モデル検査は、モデルのすべての状態と遷移を体系的に調べる手法で、確かめる性質は線形時相論理（LTL）や計算木論理（CTL）で書く。定理証明は、Isabelle や Coq などの定理証明支援系を使って形式的に推論する手法で、ふつうは完全には自動化されず、人がシステムへの理解をもとに進める。
例
Rust には次のようなツールがある。