50年経っても議論は尽きない――「形式検証」は本当に開発を救うのか？

ソフトウェアの信頼性を担保する技術として期待されながら、誕生から50年が経過した今なお賛否が分かれる「形式検証（Formal Verification）」。なぜ現場での普及は進まないのか、そして現代の開発環境において本当に必要な技術なのかを再考します。

記事を読まずにタイトルだけで判断すると少し誤解を招くかもしれない。これは1979年に発表された形式検証を批判する有名な論文への回答なんだ。振り返ってみると、その論文の強力な主張のほとんどに異議を唱える結果にはなっているけれど、一部には今でも価値がありそうな内容も含まれているよ。

「対照的に、仕様書の方が実装よりも非公式な要件に近い（だから間違いを見つけやすい）」っていう主張があるよね。でも大学で形式検証を学んだとき、自分はまったく逆だと感じたんだ。それが、形式仕様や形式検証が自分にとって魅力的でないと感じた大きな理由だった。

Lipton/Perlis/De Milloの論文なんて何年も見てなかったな。あの議論が起きた当時に自分もいたよ。歳がバレるな。彼らが推進していたのはミューテーション解析[1]だ。これはテストスイートをテストするためのテストで、プログラムにランダムな変更を加えてテストスイートがそれを検知できるかを見るというもの。ファジングはその概念に近い。形式検証が一般化するまでに時間がかかりすぎたんだ。自分が50年近く前に取り組んでいたのがこれ[2]。問題の一部は、形式手法が好きな人たちばかりが関心を寄せていたことにある。ほとんどの研究者が使う記法はひどかった。Lipton/Perlis/De Milloの論文でも指摘されている通りだ。プログラミング言語に合わせた記法が必要なんだよ。当時すでに基本的なアーキテクチャはあった。簡単な部分にはSATソルバーを、難しい部分にはAIっぽい機能を持つものを使うという構成だ。簡単な部分にはOppen-Nelsonの簡約器（最初のSATソルバー）、難しい部分にはBoyer-Mooreの定理証明器を使っていた。これぞ古き良きAI（Good Old Fashioned AI）で、1970年代後半にしては非常に優秀だった。SATソルバーが検証条件の9割以上を片付けてくれる。そこからAIソルバー向けに抽象的で難解な問題を作るような検証記法が欲しくなる。例えばアサーションを2行続けて書いて、難しい方の問題を最初のアサーションから次を証明することにする、といった具合だ。当時は計算能力が足りなかった。Boyer-Mooreの定理証明器でペアノの公理のようなものから数論を構築するのに、VAX 11/780で45分くらいかかったものだよ。今なら1秒くらいだ。数年前にBoyer-Mooreの定理証明器をGNU Common LISPに移植したんだが、再び動くのを見てみたかっただけさ[3]。LLMが面倒な作業を担ってくれる今、労働集約的な作業は大幅に減っている。LLMが吐き出すゴミを制御するためには、本当にこれが必要だ。最適化すべき具体的な目標があれば、LLMでのコーディングはずっと効果的になる。形式仕様を書くのは今でも大変だけど、仕様は単純なのに効率的な実装が難しいソフトは多い。ファイルシステム、データベース、ネットワーキング、一部の制御システムとかね。正しく動作することが不可欠なものばかりだ。

仕様が弱点だってことはみんな知ってる。でも、これは見当違いな議論だよ。だって、実装が保証されてしまえば、最後に残る脆弱な部分は仕様そのものだけになるからね。少なくとも攻撃対象領域（アタックサーフェス）を減らすことにはなるんだから。

もしソフトウェアに通常の保証規定が適用されるなら、ソフト会社なんてあっという間に潰れてしまうだろうね。形式検証があれば、そのあたりの法律も変わってくるかもしれないな。

少しクリックベイトなタイトルだと思うけど、検証の社会的側面は本物だよ。PRを出した後の作業の8割は、アイデアを周知して関係者と合意を形成することだからな。

問題なのは、AI支援の形式手法で良い結果を出せている人たちが、もともとAIなしでも形式手法で良い結果を出せる人たちだっていう点なんだ。彼らは今のAIから得ている恩恵を、将来他の人がどう恩恵を受けるかに当てはめて推測している。そこが問題の火種だよ。形式手法を正しく使うには、どの抽象度でシステムを記述するか（検証を扱いやすくするため）、どうやって正当性プロパティを記述して評価しやすくするか、といった職人芸がかなり求められる。現状のAI支援があったとしても、ユーザーは少なくともシステムの仕様や正当性プロパティを理解できるくらいには形式手法を知っておく必要がある。これって、AI登場以前に形式手法を学ぶ労力の9割を占めていたものだよ。でも、いつかAIが自力で正当に形式手法を使えるようになり、手法を知らない人たちも恩恵を受けられるようになるという希望はある。今でもAIがそれをこなすことはあるけど、手法を知らない人にとっては十分な精度じゃないこともある。近い将来、AIがもっと信頼性高くできるようになる可能性は十分ある。ただ、そうすると「AIの未来」を推測するという難問にぶつかるんだ。形式手法を扱う職人技を乗っ取れるAIに「できないこと」を予測するのは非常に難しい。AIが形式手法を使いこなせつつ、要件の収集や自律的なソフト構築はできない、あるいは作るべきソフトのアイデアさえ思いつかない、はたまたソフトの「ユーザー」そのものを置き換えられない、なんて考えるのは恣意的だと思う。言い換えれば、もしみんなが「AIが検証を肩代わりしてくれれば、要件の検証に集中できる」と思っているなら、「検証ができるAIなら、要件の検証だってできるはずじゃないか？」という疑問がわく。さらに言えば、「どうしてAIがユーザー自体を置き換えられないと言い切れるんだ？」ってことになるよね。

Rustで分散アルゴリズムを書いたとしよう。それを検証するために、TLA+で改めてアルゴリズムを記述し、その仕様をモデル検査して、必要な特性を満たすことを証明するかもしれない。これで手元には2つの成果物ができる：TLA+仕様→証明済み、Rust実装→実行可能。でも証明で確定するのは「TLA_Spec ⇒ 安全性」みたいな関係だ。実際に必要なのは「Rust_Program ⇒ 安全性」なんだよね。これがモデルとコードの乖離（model-code gap）と呼ばれるものだと思う。対処法はあるみたいだけど、分かりやすくて真似しやすいアプローチにはまだ出会えていない。

いつも思うんだけど、「形式検証って、それが検証対象にしているプログラムより正しいって、なんで言い切れるの？」という疑問があるんだ。検証エンジン自体のバグの話ではなくて、プログラムのために作成した仕様の話ね。大きな問題じゃないかもしれない。形式検証が正当性へのアプローチに役立つ便利なツールだというのは同意するよ。でも説明させて。プログラムは何か問題を解決するために書かれる。正しく解決できればバグはなく、誤っていればバグがある。複雑な問題だと、正しく解決するのは非常に難しい、というか不可能に近い。なのに、形式検証の仕様がプログラム自身よりも正しいという前提はどこから来るんだろう？どちらも非常に複雑な問題を解こうとしているのに。sel4のgitの変更履歴を読んで、OS側のバグ修正と仕様側の修正がそれぞれどのくらいあるか確認しようとしたことがあるんだ。残念ながら明確な結論は出せなかった。なぜなら、彼らはほとんどの場合、両方を同時に修正しなければならないからだ。OSのバグを見つけることは仕様の欠陥を意味し、仕様のバグを見つけることはOSにバグがある可能性を意味するからね。

今年はLeanを使って「vibe coding（感覚的なプログラミング）」をたくさんやってきたよ。分かったのは、自分が守りたい保証にとって不可欠な不変量（invariant）を特定できさえすれば、Leanは素晴らしいってこと。自分専用の形式検証済みワークフローエンジンを作ったけど、CadenceやTemporalの落とし穴と基盤をすでに知っていたから簡単だった。あと、あまり知られていないようだけど、LeanからCにコンパイルするライブラリをエクスポートできるんだ。それを使えば検証済みでパフォーマンスの高いコードが得られるし、他の場所からCバインディングとして簡単に呼び出せる。Lean自体には一般的なIOスタックはないけど、小規模なプロジェクトなら十分使えるよ。ただ、ライブラリのエクスポートやnative_decideには注意点がある。CのABIにエクスポートした時点でLeanカーネルのスコープ外になるから、コンパイラ自体からバグが混入する可能性があるんだ。