Claudeによる形式検証：123のオープンソースライブラリに証明

10月22日、AnthropicのFrontier Red TeamはTheorem社と共同で研究を発表しました。この研究でClaudeは、OSS-Fuzzプロジェクトに含まれる123のオープンソースライブラリについて、安全性の形式的な証明を書きました。証明の対象はソースコードではなく、コンパイル済みのRISC-Vコードです。著者らによると、AIを使って本番ソフトウェアをアセンブリレベルでこの規模で形式検証したのは初めてだといいます。

Claudeによる形式検証の仕組みは？

形式検証とは、誰かがテストした入力だけでなく、考えられるすべての入力に対してプログラムが特定の性質を持つことを数学的に証明することです。問題は、これまで専門家が何年もかけないとできなかったことです。研究にある比較では、seL4カーネルの検証には約20人年かかり、カーネルを書くのにかかったのは2人年でした。

研究のパイプラインは次のとおりです。

1. 出発点は、OSS-Fuzz（ライブラリにランダムなデータを絶えず浴びせ続けるGoogleのプロジェクト）にある既存のファジングテストです。
2. ライブラリをテストと一緒にRISC-Vの実行ファイルにコンパイルします。
3. Theoremが用意したRISC-VプロセッサとLinuxプロセスのセマンティクスから、仕様が自動的に生成されます。プログラムは常に正常終了し、メモリエラーもアサーション失敗も起こさないこと、という仕様です。
4. Claudeが証明を書き、Rocqの証明チェッカーが、その証明が仕様を満たしていることを確認します。
5. Claudeがバグに当たると、コードにパッチを当て、仕様を再生成して、証明をゼロから作り直します。

保証の範囲は、64MB未満のすべての入力と、モデル化されたすべてのシステム応答およびメモリ配置です（RISC-VとLinux上の静的リンク・シングルスレッドのプログラムを前提とします）。

Anthropicが示した数字は？

1. 123ライブラリで239のエントリポイント。
2. Rocqの証明は合計で約1億8,000万行。典型的な証明は約60万行で、RISC-V命令数の中央値が1万8,000のプログラムを対象にしています。
3. 全体にかかったのは数週間です。
4. 36の小さなタスクでは、Opus 5.5が半数を証明し、Opus 5より約40%少ないトークンで済みました。共有ワークスペースで作業したエージェントは、単独のときより17%少ないトークンで済んでいます。

興味深いことに、cpp-httplibの証明では、libc++の赤黒木の深さが対数的に抑えられることを示す必要がありました。そうしなければ、std::setのデストラクタでのスタックオーバーフローを排除できなかったからです。

Claudeはどんなバグを見つけたのか？

著者らによると、このプロセスで何年ものファジングをくぐり抜けてきた数百のバグが見つかりました。記事にある例は次のとおりです。

1. 展開処理（デコンプレッサ）のカウンタのアンダーフローによるバッファ外への書き込み。ただし、まれな構造を持つ約20MBの入力でしか起きません。
2. 画像デコーダのバッファ外読み取り。64MBの入力と2GB以上のメモリが必要でした。
3. 同じファイルに対する2つのハンドルで特定の順序の呼び出しを行ったときだけ現れるバッファ外読み取り。
4. libexpatのCVE-2026-56132の再発見（深くネストした入力が必要でした）。
5. ロジックのバグ：ファイルへのアクセスを制限する関数が、何もクラッシュしないのに常には機能していませんでした。

さらに追加の実験が3つあります。ClaudeはRFC 1950の形式仕様を書き、Linuxカーネルのzlibがそれを正しく実装していることをx86バイナリ上で証明しました。また、Pythonのサブセットを実行するインタープリタをRustで作り、170万のランダムなプログラムのうち99.95%でCPythonと同じ振る舞いをしました。そして、人気のPDFリーダーを検証しようとした試みでは、通常1年間に報告されるのと同じくらいのセキュリティバグが1週間で見つかりました。

PHP2ShellやBank of AmericaでのClaude Mythosと同じ流れです。AIモデルが、人間や従来のツールが何年も見逃してきたバグを見つけています。ただし今回は、パッチだけでなく証明で締めくくられています。

注意すべき点は？

1つ目は、「検証済み」が何を意味するかです。著者らは、形式検証はバグのないコードを意味しないとはっきり書いています（原文は「»Formally verified« does not mean »bug-free.«」）。証明の確かさは、仕様、RISC-VとLinuxのモデル、そしてRocqチェッカー自体の確かさを超えません。

2つ目は、範囲です。証明の対象はmuslを使った静的リンク・シングルスレッドのRISC-Vバイナリですが、私たちの多くはglibcを使ったx86やARMでコードを動かしています。また、デッドコードや、ライブラリを呼び出す側のプログラムがメモリを壊すケースもカバーしていません。

3つ目は、コストです。1つの証明で数億トークンを消費することもあり、著者ら自身がこれを最大の制約だとしています。

証明の一部はすでにGitHub（oss-verify-proofs）で公開されており、RISC-VとLinuxのセマンティクスも公開されています。残りは、未修正のバグを明らかにしてしまうおそれがあるため、公開を待っています。

よくある質問

形式検証とは？

コードがすべての入力に対して特定の性質を持つこと（たとえば、バッファの外に決して書き込まないこと）を、プログラムがチェックする数学的な証明です。テストやファジングは選ばれたケースしか確認しません。

検証済みのライブラリにはバグがないのか？

いいえ。証明が保証するのは、記述されたモデル（RISC-V、Linux、64MB未満の入力、シングルスレッド）の中でクラッシュしないことだけです。バグは仕様の中、マシンモデルの中、あるいはその範囲の外に潜んでいる可能性があります。

自分のプロジェクトを検証できるか？

Theoremは、選ばれたオープンソースプロジェクト向けの無料プログラムOSS Verifyを運営しています。OSS-Fuzzと同様に、プロジェクトのメンテナーがproject.yaml、Dockerfile、build.shを含むプルリクエストで申し込みます。ビルドを静的なriscv64バイナリに移行する必要がある点は覚悟しておきましょう。