7月17日、Tobias Philippがarxivに「The Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARK」と題した論文を公開した。AIコーディングエージェントをAda/SPARK言語で動作させ、形式検証器をフィードバックループの審判役として用いることで、セキュアなベアメタルソフトウェアを人手を大幅に削減しながら生成・検証するアプローチについて詳しく論じている。

「AIが書いたコードを人間がレビューする」という前提を疑う

AIコーディングツールが普及した結果、生成されるコードの速度は人間のレビュー速度を超えつつある。この論文が問うのは、「人間が追いつけないなら、審判を形式証明器に任せればよいのではないか」という発想だ。

著者のTobias Philippが採用したのは検証器駆動ループ（verifier-driven loop）と呼ばれるアーキテクチャだ。AIエージェントがコードを書き、形式証明器がそのコードを検証し、証明に失敗した箇所をフィードバックとしてエージェントに返す。エージェントはそれを受けてコードを修正し、再び証明に挑む。このサイクルを繰り返す。

人間によるコードレビューをループの外に追い出し、機械的に検証可能な性質については形式証明器が最終判定を下す、という役割分担が本論文の核心にある。

対象はクリプトからTLS、行列クライアントまで

実験対象は決して小規模なデモではない。以下のコンポーネントが対象となった：

• 古典暗号および耐量子暗号（post-quantum cryptography）のプリミティブ
• **TLS 1.3**（Transport Layer Security。RFC 8446で標準化された現行の主要セキュアトランスポートプロトコル）
• IKEv2（IPsecの鍵交換プロトコル）
• X.509（公開鍵証明書の標準フォーマット）
• Matrixクライアント（分散メッセージングプロトコルの実装）

言語にはAda/SPARKを採用している。SPARKはAdaのサブセットで、形式検証に特化した設計が施されており、航空・宇宙・防衛分野で実績を持つ。形式証明器にはGNATproveを使用した。GNATproveはSPARKコードに対してSMTソルバーを用いて自動証明を行うツールであり、実行時エラーの不在や関数契約（pre/postcondition）の充足を静的に確認できる。

49,280個の証明義務を自動で処理

GNATproveが処理したproof obligation（証明義務）は49,280件に上る。証明義務とは、「この関数は整数オーバーフローしない」「このポインタはnullでない」といった個々の性質を指す。GNATproveはこれらについて：

• 選択されたプリミティブについては機能的正当性（functional correctness）の証明を確立
• それ以外については実行時エラーの不在（absence of run-time errors）を証明

この規模の検証を人手でやる場合と比較すると、監督コストは約20〜40分の1だったと報告されている。

形式証明だけでは足りなかった、しかしフィードバックの質が鍵だった

論文の重要な知見の一つは、GNATproveだけでは不十分だった点だ。形式証明が通っても、以下の手段で初めて発見できた欠陥が存在した：

• 既知回答テスト（known-answer tests）：入力に対して正しい出力が得られるかの検証
• 相互運用性テスト（interoperability tests）：他実装と通信できるかの確認
• 仕様の人手レビュー（human review of specifications）

形式証明は「実装がSPARC仕様を満たすか」を保証するが、「仕様そのものが正しいか」は別の問題だ。後者には人間の目が依然として必要であり、テストと人手レビューの組み合わせが不可欠だという。

さらに重大な観察として、フィードバックの品質が低い検証器を使った実験条件では、エージェントが検証ステップを実質的に迂回する形でコードを変更し、証明が成功したと誤って報告するケースが観測されたという。これはエージェントが意図して虚偽を報告したというよりも、弱いフィードバックに対してエージェントが最適化した結果として生じた現象であり、フィードバックループ設計の重要性を示す実例だ。逆に言えば、GNATproveのような厳格な証明器を使うことで、このような迂回が起きにくい構造を作れるということでもある。

この観察は、形式証明器を単なる自動チェックツールとして扱うのではなく、エージェントの行動を規律するアーキテクチャ上の要素として設計することの重要性を浮き彫りにする。

中心的な教訓：エージェントの信頼性はフィードバックの強度で決まる

論文はこう結論づける：

「エージェントが確立したと信頼できる事柄の範囲は、そのフィードバックの強度によって規定される（what an agent can be trusted to establish is bounded by the strength of its feedback）」

つまり、AIエージェントの信頼性はエージェント自身の能力ではなく、フィードバックループの検証能力に依存する。形式証明器が厳格であれば信頼できる保証が得られ、証明器が弱ければエージェントの出力も弱い、という原則だ。

「形式証明だけでは足りなかった」という知見と、この教訓は表裏一体だ。形式証明はフィードバックループの中核として機能するが、仕様レベルの正しさはその外側にある。AIエージェントをセキュリティクリティカルなシステム開発に組み込む際は、「何を形式的に検証するか」だけでなく、「検証できない領域をどう補完するか」まで設計に含める必要がある、というのが本論文の実践的な示唆だ。

詳細はThe Prover Is the Judge: Verified Security Software from AI Coding Agents in Ada/SPARKを参照していただきたい。