Anthropic、Claudeで123のOSSライブラリを形式検証　239のテスト入口で「条件付きでクラッシュしない」を証明

従来のファジングは、生成した入力を大量に試してクラッシュを探す方式です。どれだけ試行を重ねても、試していない入力にバグがないままであることは示せません。今回の研究は、既存のファズテストを「このテストはどんな入力でも常に通る」という仕様に変換し、それを数学的に証明します。証明の対象はソースコードではなく、RISC-V向けにコンパイルされた命令列です。64MB未満のすべての入力に対して、メモリ安全性のエラーやアサーションの失敗なしにプログラムが正常終了することを示します。ただし前提条件があります。プログラムは単一スレッドの静的バイナリで、メモリ予算は固定、実行環境はモデル化されたRISC-VとLinuxプロセスの意味論です。

証明の規模は、典型的な1件で約60万行、対象バイナリの中央値は1万8000命令です。Anthropicは「これはライブラリにバグがないことを意味しない」と強調しています。残るバグは、信頼する構成要素の中か、証明の対象範囲の外にあります。

証明を試みる過程そのものがバグ発見の手段になりました。Anthropicによると、過程で数百のバグが見つかり、Claudeが修正し、修正後のコードで証明し直しました。ファジングでは入力サイズが1MB程度に抑えられるのが一般的ですが、見つかったバグには約20MBの入力で起きるカウンタのアンダーフローに伴う境界外書き込み、64MBの入力と2GB超のメモリを必要とする画像デコーダの境界外読み取りがあり、既知の脆弱性CVE-2026-56132の再発見も含まれます。

コストの低減も示されています。実OSS-Fuzzコードから作った36の小さな検証タスクで、Opus 5.5はOpus 5に比べ約40%少ないトークンで半数を証明しました。エージェント同士が証明を共有できる作業場を与えた場合は、単独作業より17%少ないトークンで済みました。証明は小さな証明の組み合わせとして再利用できるため、共有依存ライブラリの証明が蓄積すれば費用が下がる、というのがAnthropicの見立てです。TheoremはOSSのメンテナ向けに同じ工程を提供するOSS Verifyプログラムを案内しており、glibc、OpenSSL、cURLを含むNixエコシステム全体を検証するロードマップを公開しています。

この研究はメモリ安全性以外にも展開しました。Anthropicは、zlibのファイル形式を定義するRFC 1950を仕様として、Linuxカーネルの実装をx86コンパイル済みバイナリのレベルで証明しました。Rustで書いたPythonインタプリタの一部をVerusで検証し、ランダム生成した170万プログラムでCPythonと99.95%一致させた実験もあります。広く使われるPDFリーダーの検証では、1週間で例年1年分に相当するセキュリティバグを見つけたと報告しています。

限界の整理は明確です。AddressSanitizerが検出できない不具合、未検証のテスト入口、ライブラリを誤って使う呼び出し側のバグ、形式モデルが実機と異なる部分は保証の外です。実環境の多くはx86やARMで動的リンクされており、証明対象のRISC-V静的バイナリとは構成が異なります。「123ライブラリが完全にバグゼロ」と読むことはできません。それでも、テストの試行回数を増やす方式に対して、定めた条件の内側で失敗が起きないことを機械的に示す工程を、AIの力で大量に回せるようになった点是です。