アンソロピック、ClaudeでOSS123本を形式検証 約1億8000万行の証明で数百件のバグ発見

　アンソロピックは10月22日（現地時間）、同社の研究ブログで、AIのClaudeを使い、オープンソースソフトウェア（OSS）のライブラリ123本について、入力が64MB未満であればクラッシュしないことを数学的に証明したと明らかにした。パートナーのTheoremと共同で取り組んだもので、コンパイル後のアセンブリ（機械語）の水準で、実際に使われているソフトウェアへAIによる形式検証を大規模に適用したのは初めてだとしている。

　対象は、グーグルのファズテスト基盤「OSS-Fuzz」にある123のライブラリ、239のエントリポイント（テスト用の入り口）。ファズテストは、半ばランダムな入力を大量に与えてクラッシュを探す手法で、すべての入力を試せるわけではない。今回は、このテストを「どんな入力でもクラッシュしない」という仕様に自動で置き換え、Claudeが証明を書いた。証明が仕様を満たすかどうかは、証明検査系「Rocq」が機械的に確かめる。

　作業は数週間で完了し、証明は約1億8000万行のRocqコードに上る。典型的な1件は約60万行で、対象バイナリの長さは中央値で1万8000命令だった。証明の過程で数百件のバグが見つかり、Claudeが自ら修正したうえで、修正後のコードを改めて証明した。libexpatの脆弱性CVE-2026-56132の再発見も含まれるという。

　一方、アンソロピックは限界も明記している。証明は、単一スレッドで動く静的なRISC-VバイナリがLinux上で動くことなどを前提とし、「形式検証済み」は「バグなし」を意味しないと強調した。

　同社は、証明の一部と、RISC-VおよびLinuxの形式モデルを公開した。Theoremは他のOSSプロジェクトにも同じ処理を実行すると申し出ており、開発者向けのClaudeスキルも公開するという。同社は20日にも、ClaudeでOSS25件の攻撃対象領域を分析し493件の問題を見つけた取り組みを公表していた。