Claudeが123ライブラリを形式検証 — OSS-Fuzz×Rocqで「64MB未満の入力でクラッシュしない」を証明した仕組みと限界

はじめに

Anthropic の Frontier Red Team が 10 月 22 日、Claude を使ってオープンソースライブラリを大規模に形式検証した結果を公表しました。対象は Google の OSS-Fuzz に登録されている 123 ライブラリ・239 エントリポイント。コンパイル後の RISC-V アセンブリの段階で、「64MB 未満のどんな入力を与えてもクラッシュしない」ことを、証明チェッカー Rocq（旧 Coq）で機械的に確かめています。証明の総量は約 1 億 8,000 万行、かかった期間は数週間です。

Hacker News では 429 ポイントを集めましたが、「形式検証済み」という言葉は誤解されやすいものです。この記事では、何がどう証明されたのか、なぜ今それが可能になったのか、そして何が保証されていないのかを整理します。

何が証明されたのか

出発点は、開発者がすでに書いているファジング用のエントリポイントです。ファジングは半ランダムな入力を大量に投げてクラッシュを探す手法ですが、入力空間を網羅することはできません。今回の取り組みは、このエントリポイントを「全入力について」の命題に格上げしました。

流れは次のとおりです。

OSS-Fuzz は C/C++ を AddressSanitizer（ASan）付きでビルドするため、不正なメモリアクセスは即クラッシュになる
協力企業 Theorem の RISC-V と Linux プロセスの形式意味論を使い、実行ファイルから「64MB 未満のどの入力でも正常終了する」という仕様（定理）を機械的に生成する
Claude がその証明を書き、Rocq が検査する
証明の途中でバグに当たると、Claude がコードを修正し、修正後のバイナリから仕様を作り直して再証明する

対象のバイナリは中央値で約 1 万 8,000 命令、証明は 1 本あたり約 60 万行です。証明コードを人間がレビューする必要はほとんどなく、信頼すべきなのは主に「RISC-V と Linux のモデル」「定理の文言」「Rocq」の 3 つ、というのが Anthropic の説明です（厳密には Rocq が依存するハードウェア・OS・OCaml コンパイラも信頼の対象に含まれると注記されています）。

成果として数百件のバグが見つかっています。約 20MB の入力と珍しいメモリ配置の組み合わせでしか起きない、伸張処理のカウンタのアンダーフローによる範囲外書き込み、64MB の入力と 2GB 超のメモリが必要な画像デコーダの範囲外読み取り、libexpat の既知脆弱性 CVE-2026-56132 の再発見などです。ファザーは通常 1MB 程度までの入力しか試さないため、こうした「巨大入力でだけ起きる」バグは見つけにくいと記事は指摘しています。

なぜ今、この規模が可能になったのか

形式検証は昔から「高すぎる」技術でした。記事が引く seL4（形式検証された OS カーネル）は、実装に約 2 人年、検証に約 20 人年かかったとされます。証明は膨大で、書ける人材も限られていました。

LLM が変えたのは、この人手のボトルネックです。目標が「Rocq が通るかどうか」という明確な判定器で決まるため、LLM は何百万行でも試行錯誤を続けられます。9 月に紹介したフェルマーの最終定理の Lean 形式化と同じ構図で、機械的な検証器がある領域では、LLM の出力の正しさを人が信じる必要がないのが強みです。

ただし、何でも通せばよいわけではありません。Claude がプログラムを「何もせず終了する」ように書き換えれば、どんな定理も証明できてしまいます。そこで今回は、パッチに減点を課し、「パッチで挙動が変わる入力がどれだけ少ないか」を証明すると加点する設計にし、パッチはすべて記録して監査しています。報酬ハックへの対策を最初から組み込んでいる点は、エージェントに自律修正をさせる際の参考になります。

効率面のデータもあります。OSS-Fuzz 由来の小さな検証課題 36 問では、Opus 5.5 は Opus 5 より約 40% 少ないトークンで半数を証明しました。複数のエージェントが証明を共有すると、トークンは単独より 17% 減り、単独では解けなかった問題も解けています。C ランタイムの初期化や ASan 周りの証明は多くのプログラムで共通しているため、使い回しが効くのです。依存関係はべき乗則に従うので、glibc・OpenSSL・cURL のような共有ライブラリを先に証明すれば、多くのソフトウェアが一気に扱いやすくなる、というのが Theorem の見立てです。

「形式検証済み」が保証しないこと

記事自身が強調しているのは、「形式検証済み」は「バグがない」という意味ではないという点です。主な穴は次のとおりです。

実行環境の差: 証明はシングルスレッド・静的リンク（musl libc）の RISC-V バイナリが対象。多くの人が使う x86/ARM の動的リンク glibc 環境とは別物
ASan の限界: ASan が検出できないメモリ安全性の違反は証明の対象外
網羅範囲: 各ライブラリの全エントリポイントを検証したわけではない
デッドコード: 全エントリポイントを検証しても、どこからも呼ばれないコードやライブラリ全体はカバーできない
呼び出し側の誤用: ライブラリが正しくても、呼び出し側がメモリを壊せば意味がない
信頼基盤の誤り: Rocq や RISC-V・Linux のモデル自体にバグがあり得る

HN で出た論点の一つも「検証（仕様どおりか）」と「妥当性確認（仕様が正しいか）」の違いでした。AI が生成した仕様や意味論を誰が確かめるのか、並行性という一番難しい部分を飛ばしていないか、という指摘です。一方で、別の事例（Linux カーネルの zlib を x86 バイナリのまま証明したもの）で Claude が x86 の命令セット意味論を生成した際には、公式リファレンスの誤りが数百件、ハードウェアのバグも少数見つかったと記事は述べており、信頼基盤を固める作業自体にも価値があることがうかがえます。

エンジニアへの影響

すぐに手元で使える話ではありませんが、実務に効いてくる点はあります。

ファズテストの価値が上がる: 今回の仕組みは、既存のファズエントリポイントをそのまま定理に変換します。往復変換（圧縮→伸張で元に戻る）のような性質を assert で書いておけば、クラッシュしないことの証明がその性質の証明にもなります。ファズテストを書いておくことが、将来の形式検証への入口になるわけです。

依存ライブラリの見方が変わる: Theorem は今回のパイプラインを OSS プロジェクトに提供し、自分のコードを検証するための Claude 用 skill も公開しています。今後 Nix エコシステムの主要パッケージに広がれば、「どの依存が検証済みか」が選定基準の一つになる可能性があります。

AI が脆弱性を見つける時代の防御: Anthropic は、LLM がすでに大規模に脆弱性を見つけている以上、防御側にはすべての経路を試す保証のないファジングだけでなく、コードの安全性を「保証」できる手段が必要だと主張しています。今週の PHP2Shell や Onigmo の件のように、パーサーや正規表現エンジンの深い部分のバグは今後も出続けるはずです。攻撃側が AI で探すなら、防御側も AI で証明する、という構図が現実味を帯びてきました。

一方で、証明の生成には数億トークンかかることもあり、個人や小さなチームが日常的に回せる段階ではありません。

まとめ

Claude が OSS-Fuzz の 123 ライブラリ・239 エントリポイントを、RISC-V アセンブリの段階で Rocq により形式検証した
証明は約 1 億 8,000 万行。過程で数百件のバグが見つかり、ファザーでは届かない巨大入力のバグも含まれる
鍵は「検証器が正しさを判定する」構造と、報酬ハックを防ぐ設計、証明の共有による効率化
ただし対象はシングルスレッドの静的 RISC-V バイナリで、ASan の外や仕様の誤りまでは保証しない

形式検証が「一部の研究者の道具」から「依存ライブラリに付く品質ラベル」へ移るかどうかは、トークンコストの低下と x86・glibc への拡張にかかっています。