横断層: 検証を実行する手段の数学

連載序論はこちら。第一〜四層が「何を主張するか」の数学だとすれば、この層は「主張をどう機械で確かめるか」の数学。

5.1 モデル検査 [実務厚]

概念: 有限状態モデルの全数（または記号的・有界）探索で時相性質を検査し、違反時は具体的な反例トレースを返す。反例が出ることが定理証明に対する最大の実務的優位——反例は設計者への教育材料になる。

道具と実績: TLA+（AmazonがS3・DynamoDB等の設計検証で、テストでは到達不能な深さのバグを複数発見したと報告。MongoDB・CosmosDBも採用）、SPIN（通信プロトコル、NASA）、Alloy（関係論理＋小スコープ、スキーマ・設計の検査に向く）、NuSMV/nuXmv（ハードウェア寄り）。

刷新での適用: 適用先の第一候補は切替手順・並走プロトコル・障害時運用。コードではなく「手順と並行性」の設計を検証する道具として使う。数千行の実装より先に、数百行のTLA+モデルで切替の論理を潰すのが費用対効果の最適点。

5.2 抽象解釈と Galois 接続 [実務厚]

概念: 具体意味論（実際の実行の集合）と抽象領域（区間・多面体・オクタゴン等）をGalois接続（α: 抽象化, γ: 具体化の随伴対）で結び、抽象側でプログラムを「実行」して全実行の過大近似を得る。健全性は随伴から従い、偽陽性はあるが見逃しはない（対象性質について）。無限上昇列を止めるwideningが実用の鍵。

道具と実績: Astrée（Airbus A380/A400Mの飛行制御Cコードで実行時エラー不在を証明した、産業的検証の金字塔）、Polyspace、Meta Inferの基盤理論（Cousot–Cousot 1977）。

刷新での適用: 資源限界系の欠陥（バッファ・ファイル容量・カウンタ溢れ・数値オーバーフロー）の網羅的検出。「このバッチ量でこのファイル上限に当たる」型の欠陥は、値域解析の守備範囲そのもの。

5.3 SMT ソルバ [実務厚]

概念: 命題論理のSATに、算術・配列・ビットベクトル・未解釈関数などの理論を組み合わせて充足可能性を判定する（DPLL(T)方式）。現代の検証ツールの共通基盤エンジンであり、Dafny・F*・有界モデル検査・シンボリック実行（KLEE）・篩型のすべてが背後でSMTを呼ぶ。

実績: Z3（Microsoft）、CVC5。SMT競技会による継続的性能向上が、2000年代以降の「検証の自動化が急に実用になった」現象の主因。

刷新での適用: 直接使うというより、「どこまで自動化できるか」の境界線を引いている技術として理解しておく。線形算術＋配列に収まる仕様は自動、非線形算術・量化子が濃い仕様は人間の補題が要る、という感覚が検証工数見積りの基礎になる。

5.4 定理証明支援系 [実績有]

概念: 人間が証明を書き、機械がその正しさだけを検査する。選んだ論理の範囲で極めて高い表現力を持ち、自動判定できない個別問題にも人間が補題を与えて取り組める——ただし決定不能性や形式体系の不完全性そのものが消えるわけではなく、人間の労働で買い戻せるのは個別問題に対する証明の構築である。信頼基盤は小さな証明検査カーネルに集約される（de Bruijn基準）。

実績: seL4（Isabelle/HOL）、CompCert（Coq）、数学側では四色定理・Kepler予想・Leanのmathlib。コスト感覚: seL4は実装1行あたり証明約20行・全体で約20人年——「小さく死活的なコア」以外にこの投資は正当化しにくい、という相場観ごと記録しておく。

刷新での適用: 適用するなら利息計算・端数処理・勘定仕訳の核アルゴリズムのみ。それ以外はより軽い手段に振るのが定石。

5.5 経験的手法との接続 — 証明とテストの連続体 [実務厚]

概念: 形式手法とテストは対立ではなく連続体をなす。性質ベーステスト（法則の経験的検査）、ファジング＋不変条件アサーション（クラッシュ以外の意味的違反も拾える）、差分テスト（二つの実装を同一入力で叩き出力を比較——現行システムをオラクルにする刷新戦略の正体）、メタモルフィック検査（正解が不明でも「入力をこう変えたら出力はこう変わるはず」という関係性質で検査——オラクル不在問題への解答）。カオス工学は「障害仮定下の不変条件維持」の本番環境での経験的検査と読める。

刷新での適用: 現実の刷新検証の主力は間違いなくこの節になる。上の各層は、この経験的検査群に「何を検査しているのか・何を取りこぼすのか」の意味論を与える役割、と位置づけるのが誠実な整理。

---

連載: システム設計と大規模刷新のための数学

1. 序論 — 地図の全体像
2. 第一層: 仕様を書くための数学
3. 第二層: 仕様と実装の関係の数学
4. 第三層: 合成の数学
5. 第四層: 不可能性と限界の数学
6. 横断層: 検証を実行する手段の数学（この記事）
7. 総括: 実績濃淡マップと大規模刷新への適用