形式手法によるソフトウェア検証：成功要因と現実的な課題

はじめに：宇宙人との交渉という比喩

本記事は、形式手法を用いたソフトウェア販売における成功と失敗を分析した前作の補完篇です。2024 年末の講演に基づく内容であり、以下の点を明確に伝えます。

• 困難な課題と高コストな課題の区別:
  • 多くの技術的課題は解決可能ですが、単に費用が高すぎるだけです。
  • 重要なのは、「不可能」ということではなく、「現在の市場条件において便益がコストに見合わない」ことです。
• 形式検証済みソフトウェアの実例:
  • 形式的に検証されたコンパイラの構築法は既に確立されています（例：CompCert）。
  • 暗号ライブラリ、パーサー、マイクロカーネルについても同様に実現可能です。
  • GCC が形式検証されていない理由:
    • 達成しようとすれば費用が非合理ほど高いためです。
    • そのコストに見合う便益を享受できる状況ではありません。

シナリオ A：形式検証された GCC（現実的なアプローチ）

仮に「形式的に検証された GCC」が必要な緊急事態が発生した場合（宇宙人シナリオの例え）、以下の通りです。

• 達成可能性: MCU 第 3 作映画（予算 220〜240 億ドル）のコストよりも低額で実現できます。
• 前提条件: G7 各国が協調し、巨額の投資を行うことができれば可能です。
• 現状の状況:
  • 形式検証を追求する研究者・エンジニアはすでに活動していますが、市場規模とコストのバランスが取れていません。
  • この分野には未開拓の大きな可能性が存在します。

シナリオ B：形式検証されたウェブブラウザ（不可能に近い課題）

もし宇宙人が「形式的に検証されたウェブブラウザ」を求めた場合、話は別です。

• 根本的な問題: 「ウェブブラウザ」という概念自体に、形式的な仕様書が存在しません。
  • Chrome には形式仕様書がないため、それを構築することはできません。
  • 人類の運命は絶望的になり、新しいコンピュータサイエンス分野を次々と発明する必要があります（MCU の予算ですら足らない可能性）。

なぜ形式仕様が難しいのか？

問題の本質は、PDF や文字処理ソフトウェアなど多くのシステムに形式的な仕様が欠落していることにあります。

• 単に「まだ誰も書き上げていない」だけでなく、**「正確で整合性の取れた仕様が書けるはずがない」**と信じる理由があります。

---

形式的仕様は形式的かつ具体的であるべき

形式的仕様の必要性について整理します。

形式的仕様の役割

• システムの動作を記述する: システムそのものではなく、その「概要・説明」として機能します（地図が地形その物ではないのと同様）。
• 検証のための土台:
  • 何も仕様がないままでは、何を検証しているのか不明確です。
  • 数学者が定理を証明したり、Rust の借用チェッカーを実行したりする際にも、対象となる「仕様」が必要です。

有用な形式仕様の 5 つの特徴（経験則）

• 数学的清浄さ: シンプルな集合体を用いて記述可能であること。
• 推論のしやすさ: 人間直感や形式的解析を通じて、システムを理解できる手段となること。
• カプセル化: システムの「内部」と「外部」の境界が明確であり、境界での挙動を記述すること。
• 合意形成: 設計者と利用者が、仕様に従うことに同意していること。
• 変化への安定性: システムが進化する際にも、仕様が大きく変わらない（差異を抽象化している）こと。

形式検証が成功するシステムの種類

以下の要件を自然に満たすシステムは、「本質的に形式化可能」と言えます。

• コンパイラ
• 暗号ライブラリ
• パーサー
• マイクロカーネル

注意点: これらは形式検証における**「ニッチ」**であり、大多数の現実世界のシステム（特に複雑なアプリケーション）には適用されません。

---

実は、形式的仕様があまりにも多い

多くの開発者は、形式的仕様なしに日常的に非形式的な仕様を使用しています。これらも事実上の「仕様」として機能します。

存在する非形式的な仕様の例

• 文章によるドキュメント: 設計書、ユーザーマニュアル、ホワイトペーパー、RFC など。
• スライド資料: 特に米国政府機関で一般的。
• システムそのもの（レガシー系）: 「現在やっていること」自体が事実上の仕様。変更＝仕様の違反となる。
• ユースケースストーリー: 利用者向けのアプリケーションにおける、実際の使用シナリオの集計（形式的表現は極めて困難）。
• テストコード: 単体テストや統合テスト（特定の入力に限定される部分仕様）。
• その他:
  • 包括参照実装
  • コード内のインラインコメント
  • チーム内の暗黙知・実践知
  • 顧客の好み
  • 規制要件

「仕様の整合性」の問題

不十分で不完全な部分仕様が多数存在し、それらが互いに整合していないケースが一般的です。

ケーススタディ：Galois のクライアント向けプロジェクト

形式検証を試みる際によく起こる対話です。

1. 質問: 「システムの仕様がありますか？」

   • 回答 A: 「2 スライドのパワーポイント資料です。」
   • 回答 B: 「半構造化された文章で、7000 ページにも及ぶ要件文書です。」

2. 検証時の矛盾:

   • 「我々はシステムが [動作 X] を行うことを発見しましたが、貴社の仕様からは [動作 Y] が導かれます。」
   • クライアント A: 「おっと、それは重要ではありません。」（優先度判断の不一致）
   • クライアント B: 「はい、6 ヶ月前にその部分を変更しました。」（仕様と実装の乖離）

結果: 数十回にわたるこのような対話が続くと、再教育が「猿芝居」と見なされ、プロジェクトは頓挫します。

形式的仕様の作成の難しさ

• 視点の違い: 形式仕様にはシステムを俯瞰するトップダウン的な視点が不可欠です。しかし、エンジニアや設計者は通常、この視点を欠いています。
• 非形式仕様の特性:
  • 曖昧で部分的で柔軟であるため、人間同士のコミュニケーションには適しています。
  • 「誤っているが有用な」記述を含んだり、一部を省略したりすることが可能です（これは強みですが、形式的記述の障壁にもなります）。

多くのシステムはトップダウン構造を持ちますが、すべての振る舞いをカバーする数学的に整合的な形式仕様を持っているのは極めて稀です。コア機能以外になるとすぐに不明確な領域に入り込み、「システムは何をするべきか」が定まらなくなります。

---

具体的な事例：Portable Document Format (PDF)

PDF は仕様化しやすいはずの標準ですが、現実には非常に困難です。

• 現状:
  • 数十億台のデバイスで動作し、明確な標準がある。
  • 多数の実装（アマチュアプロジェクトから重要システムまで）が存在する。
  • しかし、実装すべき内容に関する合意がない。
  • 既存の実装と一致する仕様も存在せず、不良/非安全なドキュメントを明確に定義できない。
• 絶望のじゃがいも（The Despair Potato）:
  • データセットには「既知の不良事例」と「既知の健全事例」があるが、それ以外の大半のドキュメントは健全か不良かわからない。
  • 理由: PDF リーダー側が標準からの逸脱を誤修正しているため。
    • 読めない場合、作成者への非難になるため、リーダー側で勝手に修復しようとする。
    • 各リーダーの解釈が異なるため、同じドキュメントでも二通りの解釈が可能になる。
• 結論:
  • PDF は形式的化できる「離散的なカテゴリ」として存在していない。「PDF とみなせるか否か」の曖昧な境界領域に存在する。

Galois の SafeDocs プロジェクトでは、専用言語「DaeDaLus」で形式仕様化を試みました。しかし、以下の課題が残りました。

1. 記述的ではない: 実際の PDF リーダーとは動作が異なる。
2. 規範的ではない: 「正しくあるべき」動作を特徴付けていない。
3. 承認プロセス不明確: より厳密で承認される仕様に至る方法が見えない。

---

結論：意図通りに行うこと

形式検証の時代は現在、**「証明のコスト」**によって支配されています。 しかし、近い将来に AI の進歩により「安価で大量の証明」が可能になったらどうなるでしょうか？

• 潜在的リスク:
  • すぐにすべてのコンパイラやマイクロカーネルを検証してしまい、そこでシステムが詰んでしまう可能性があります。
  • 「何を望むべきか」という指示すら AI（例：Claude）から得られない状況になるかもしれません。
• 戦略的な推奨:
  • 完全で整合的な形式仕様を書くことは大多数のシステムで極めて困難です。
  • それに代わる**「限定的で部分的な仕様」**（テストケースなど）を活用し、すぐに有用でありながら開発チームに過度な負担をかけないアプローチが必要です。

「仕様作成はバグを引き出す」という陳腐な格言について

• 悲観的な見方: いかなる道具も思考を明確化する負担を取り除けない。仕様も例外ではない。
• 希望的見方: プログラミングのように、慎重なツールの設計で数億人が利用可能なレベルまで持てば、仕様にも同じことができるかもしれません。

まとめ: 我々はちょうどスタートしています。やるべきことは多くあり、常に「宇宙人（即ち、検証不可能な要件）」の存在を見失わないよう注意する必要があります。