LOG ENTRY / post
システム設計のための数学 総括: 実績濃淡マップと大規模刷新への適用
総括: 実績濃淡マップと大規模刷新への適用
連載序論はこちら。連載で扱った手法群を一覧に畳み、大規模刷新のフェーズごとにどこが効くかを対応付ける。
実績濃淡マップ
| 手法/概念 | 成熟度 | 代表実績 | 刷新での主用途 |
|---|---|---|---|
| ホーア論理・契約 | 実務厚 | SPARK Ada, Dafny | 変換処理の正当性 |
| 時相論理＋モデル検査 | 実務厚 | Amazon TLA+, ハードウェア | 切替手順・並行性 |
| 分離論理（バグ検出振り） | 実務厚 | Meta Infer | C/C++資産解析 |
| 性質ベース/差分テスト | 実務厚 | QuickCheck系, 各社CI | 新旧照合の主力 |
| 抽象解釈 | 実務厚 | Astrée (A380) | 資源限界・溢れ検出 |
| SMT | 実務厚 | Z3（各ツール基盤） | 自動化の共通基盤 |
| CRDT / CALM | 実務厚 / 実績有 | Riak, Cosmos DB | 照合系の調整レス化 |
| 帰納的不変条件 | 実務厚（文化） | Paxos証明, IC3 | 刷新全体の背骨 |
| 精緻化 (B/Event-B) | 実績有 | パリ地下鉄14号線 | 勘定核の段階的導出 |
| 依存型・定理証明 | 実績有 | seL4, CompCert | 死活的コアのみ |
| 振る舞い部分型 | 実務厚（原則） | Liskov原則, Pact | 外部互換性の定式化 |
| Rely-Guarantee | 実績有 | ハードウェアAG | 並走期の相互依存分析 |
| 双模倣・余代数 | 理論先行 | mCRL2 | 差分テストの意味論 |
| セッション型 | 理論先行 | Scribble | 電文プロトコル記述規律 |
| 関手的データ移行 | 理論先行 | CQL | 移行写像の分類語彙 |
| LTL合成 | 理論先行 | GR(1)ロボティクス | 仕様実現可能性検査 |
大規模刷新への適用マッピング
考古学（現行仕様の発掘）: LLMによる仕様逆生成＋性質ベーステストでの検収（1.5, 5.5）。発掘した性質は帰納的不変条件の候補台帳（2.2）として蓄積する。ここは数学よりも「数学に乗せられる形式で仕様を書き溜める」規律が本体。
移行設計: データ対応を抽象化写像として明示し可換性を検査（2.4）。多対一の潰しはΣ/Δ/Πの分類で漏れ点検（3.5）。移行バッチ単体は事前・事後条件で契約化（1.1）。
並走・照合: 差分テストの意味論的限界（トレース同値の有限近似、2.3）を明記した上で主力に据える（5.5）。照合系は単調設計で調整レス化（3.4）。新旧の相互依存はrely-guaranteeで障害連鎖を列挙（3.1）。
切替手順: TLA+等で手順・並行性を小さく抽象化して全数検査（1.2, 5.1）。「分断・不一致時にどちらを正とするか」はCAP的経営判断として事前確定（4.2）。
互換性維持: 外部接続ごとに振る舞い部分型の条件（事前弱化・事後強化のみ）で点検（3.2）。
資源限界: 容量・溢れ系は抽象解釈ツールで網羅（5.2）。
死活的コア: 利息・端数・仕訳の核だけ精緻化 or 定理証明（2.1, 5.4）。
検証ポートフォリオ設計: Riceの定理由来の四極（健全な過大近似・過小近似・決定可能断片への制限・手動証明）に性質を割り当てる表を作る（4.1）。全性質に同じ手段を使おうとしない。
追記（2026-08-21）: 全層統合の最新事例と正誤表
公開直後、GPT-5.6 Solによる本連載の徹底レビューを受けた。主要な指摘と新出典を独立に裏取りした上で、価値の高いものを本文に反映した。経緯ごと記録として残す。
全層統合事例: AWS Nitro Isolation Engine
2026年、この地図のほぼ全層を一つの本番システムで統合した事例が出ている。AWSのNitro Isolation Engine——EC2のVM分離だけを専任で担う最小の信頼基盤で、re:Invent 2025で発表され、Graviton5世代インスタンスの標準機能として一般提供された。Rustのサブセットで実装し、事前・事後条件、分離論理、精緻化、非干渉性を組み合わせてIsabelle/HOLで機能的正当性と分離特性を検証。機械検査済みの数学は約33万行で、seL4に匹敵する規模と報告されている（AWSの解説記事）。注目すべきは、ハイパーバイザ全体を証明したのではなく、分離を担う小さなコアへ信頼境界を縮めてから証明した点で、「定理証明は小さく死活的なコアに限定する」という本連載の相場観（5.4）の最新かつ最大級の実例になっている。
また、LLMによる検証済みコード生成のリポジトリ規模ベンチマーク（実装と証明の同時生成を測るVero等）では、単一関数で通る成功が複数モジュールの合成に伸びない傾向が一貫して報告されており、「合成」を独立の第三層に置いた判断の傍証といえる。
正誤表
| 箇所 | 誤 | 正 |
|---|---|---|
| 4.1 Riceの三分類 | テスト・有界検査を「完全だが不健全」と分類 | 健全な過大近似と過小近似（反例は本物・見逃し許容）の枠へ修正。bound内で網羅的でも無反例は無制限の安全を意味しない |
| 5.4 定理証明 | 「表現力は無制限」 | 選んだ論理体系に相対的。決定不能性・不完全性は消えない |
| 1.1 最弱事前条件 | wpを部分正当性の文脈で説明 | Dijkstraのwpは停止込みの全正当性側。部分正当性側はwlp |
| 3.4 CRDT | 結び半束をCRDT一般の説明として記述 | 半束はstate-based CRDTの説明。op-basedは可換性＋因果配送 |
| 3.4 Figma | CRDTの実戦場として例示 | Figmaは自社解説で「true CRDTではない」と明言するCRDT-inspired方式 |
このほか、精密化のみの軽微な修正（safety/livenessの「積」→「共通部分」、精緻化の前順序性、CAPが構造的類推であることの明記、Σ/Δ/ΠのKan拡張としての正確化、validationの境界の言い直し、旧系オラクルの既知バグ凍結問題の追記）を各記事に反映した。
レビューではさらに、新旧等価性を複数実行間の関係として扱うhyperproperties、形式モデルと実装の乖離を検査するconformance checking、業務不変条件ごとの調整回避可能性を扱うI-confluence、保証の前提と失効条件を管理する「保証台帳」など、この地図に未収載の重要概念が指摘された。これらは第二期として稿を改めて扱う。
較正の注記（この連載自体の信頼度）
- 各手法の存在・定義・代表事例（seL4, CompCert, Astrée, Météor, Amazon TLA+等）は確立された公知の事実で、確信度は高い。
- 数値の細部（seL4の証明行数・人年など）は桁は正しいが端数は資料により揺れる。引用時は一次資料の再確認を推奨。
- 「刷新での適用」は本連載独自の対応付けであり、実プロジェクトでの検証実績があるものではない。仮説として扱ってほしい。
- 成熟度三段階の判定は執筆時点の主観的較正。特にLLM×形式手法（不変条件生成・仕様逆生成）は変化が速く、この評価は早期に陳腐化しうる。
主要文献
- Leslie Lamport, Specifying Systems（TLA+の正典、無料公開）/ Hillel Wayne, Practical TLA+
- Baier & Katoen, Principles of Model Checking（モデル検査の標準教科書）
- Daniel Jackson, Software Abstractions（Alloyと小スコープ仮説）
- Jean-Raymond Abrial, Modeling in Event-B（精緻化の工学）
- Benjamin Pierceほか, Software Foundations（Coqで学ぶ第一層、無料公開）
- Davide Sangiorgi, Introduction to Bisimulation and Coinduction
- Glynn Winskel, The Formal Semantics of Programming Languages
- Cousot & Cousot (1977), "Abstract Interpretation" / Rival & Yi, Introduction to Static Analysis
- David Spivak, Category Theory for the Sciences / Fong & Spivak, Seven Sketches in Compositionality（無料公開）
- Marc Shapiro et al. (2011), "Conflict-free Replicated Data Types" / Hellerstein & Alvaro, "Keeping CALM" (CACM 2020)
- Newcombe et al., "How Amazon Web Services Uses Formal Methods" (CACM 2015)
- Klein et al., "seL4: Formal Verification of an OS Kernel" (SOSP 2009) / Leroy, "Formal Verification of a Realistic Compiler" (CACM 2009)
連載: システム設計と大規模刷新のための数学
- 序論 — 地図の全体像
- 第一層: 仕様を書くための数学
- 第二層: 仕様と実装の関係の数学
- 第三層: 合成の数学
- 第四層: 不可能性と限界の数学
- 横断層: 検証を実行する手段の数学
- 総括: 実績濃淡マップと大規模刷新への適用（この記事）