形式検証とは — 数学的証明で安全を担保する考え方とSDVでの使いどころ
形式検証（ソフトウェアの正しさを数学で証明する手法）は、「テストではなく数学的証明で安全性を担保する」という発想の転換を実現する技術である。本記事は、形式検証がテストと何が根本的に違うのか、どんな手法があるのか、そしてSDV（ソフトウェア・デファインドな車）開発でどこに使うのが合理的かを整理する。結論を先に言えば、形式検証は「すべてのソフトに適用する技術」ではなく、安全クリティカルな最小限の領域に集中適用して、システム全体の安全を構造的に保証する技術である。
形式検証とは何か
形式検証とは、システムが仕様を満たすことを、すべての可能な入力に対して数学的に証明する手法である。AIの確率的な挙動が安全に関わるシステムに入り込むSDV時代に、テストでは到達できない安全保証を与える手段として注目されている。
テストと形式検証の根本的な違い
テストは「特定の入力に対して期待どおりの出力が得られた」ことを確認する行為だ。100万件のテストに合格しても、「100万1件目で失敗しない」保証はない。テストの限界は「テストしていないケースについては何も言えない」ことにある。
形式検証は「すべての可能な入力に対して仕様が満たされる」ことを数学的に証明する。テストが有限個のケースを確認するのに対し、形式検証は無限の入力空間全体をカバーする。この違いは安全設計で決定的な意味を持つ。最高水準の機能安全（ASIL-D）でも要求は「十分な」テストカバレッジだが、膨大なパラメータを持つAIモデルの全入力空間をテストすることは物理的に不可能だ。形式検証は、テストでは原理的に不可能な「すべての入力に対する保証」を与えうる、数少ない手法である。
主要な二つの手法——定理証明とモデル検査
形式検証には大きく二つのアプローチがある。
| 手法 | やり方 | 特徴 |
|---|---|---|
| 定理証明 | 人間が証明の骨格を設計し、証明支援系が機械的に正しさを検証 | 深い性質を証明できるが人手を要する |
| モデル検査 | 有限状態モデルの全状態遷移を網羅的に自動探索 | 自動化しやすいが「状態爆発」の制約がある |
自動車では両者の併用が現実的だ。OSの中核（カーネル）レベルの安全性は定理証明で証明し、プロトコルや状態遷移の検証にはモデル検査を使う、という多層的な戦略になる。定理証明にはIsabelle/HOL・Coq・Leanなどの証明支援系が、モデル検査にはTLA+などのツールが使われる。
seL4——形式検証の到達点
形式検証の実績として基準になるのが、seL4（マイクロカーネル）の検証である。約1万行のCコードに対し、抽象仕様・実行仕様・C実装の三層が完全に一致すること（精緻化関係）が、定理証明によって示された。これにより「カーネルが仕様と異なる動作をしない」「ある仮想マシンが他の仮想マシンのメモリを侵害しない」「情報が許可された経路以外を流れない」ことが数学的に保証される。この隔離保証が、安全度の異なる機能を同一基盤に同居させる混在クリティカリティ設計の土台になる。
AIモデルの形式検証——発展途上のフロンティア
カーネルの形式検証は確立技術だが、ニューラルネットワークの形式検証は発展途上だ。ネットワーク構造と安全特性を入力に「その特性を満たすか／反例があるか」を判定する検証器（Marabou、α,β-CROWN等）が研究されているが、産業レベルでは課題が残る。ネットワーク規模の増大に伴う演算時間の爆発、証明できる入力変動の種類の限定、悪天候やセンサーノイズのような複雑な想定外入力への適用の難しさ——これらは、AIモデルの完全な形式検証が当面は困難であることを意味する。
SDVでの使いどころ——「選択的適用」の設計思想
現実的なSDVでは、形式検証は「すべてに適用する」のではなく「安全クリティカルな層に集中適用する」のが合理的だ。安全度の最も高い決定論的な安全制御領域（seL4カーネルと、異常時に安全側へ倒すロジック）は形式検証の対象とし、「すべての入力に対して安全な動作が保証される」ことを証明する。一方、AI推論領域はテストとシミュレーションで検証し、その出力を形式検証済みの安全制御が監視・制約・封じ込める。
この「形式検証済みの安全基盤＋テストベースのAI推論」の二層構造は、AIの安全規格（ISO/PAS 8800）のAI安全論証で最も強力な論拠になる。「AIは誤りうるが、アーキテクチャ全体としては形式検証済みの介入によって安全が担保される」——テストだけでは到達できないこの論証こそ、形式検証のSDVでの価値の核心である。
まとめ：形式検証は「集中適用」で効く
形式検証は、テストの限界（未テストのケースは保証できない）を、数学的証明（すべての入力を保証する）で超える手法である。ただし全ソフトには適用できないため、安全クリティカルな最小限の領域に集中適用し、システム全体を構造的に守るのが実務的な設計思想になる。自社で具体化する際の論点は次のあたりだ。
- どの領域を形式検証の対象（安全の最後の砦）として切り出すか。
- AI推論を、形式検証済みの安全制御でどう監視・制約するか。
- 定理証明とモデル検査を、どの階層にどう使い分けるか。
機能安全の全体像はISO 26262と機能安全・ASILの構造を、AIの安全保証はISO/PAS 8800と車載AIの安全を、SDV全体像は【SDV入門】経営層が掴むSDVの全体像をあわせて参照してほしい。自社の安全アーキテクチャに即した形式検証の適用範囲の設計は個別性が高く、具体化の段階では外部の視点を入れると論点整理が速い。