Anthropic、Claudeで123ライブラリを形式検証

Anthropicは2026年10月22日、Theoremとの共同研究で、Claudeを使い、オープンソースソフトの安全性をアセンブリコード水準で形式検証したと発表しました。GoogleのOSS-Fuzzにある123ライブラリの239エントリーポイントについて、一定条件下で64MB未満のあらゆる入力に対してクラッシュしないことを証明し、検証の過程では長年見逃されてきた不具合も発見・修正しました。

研究チームは、既存のファズテストを「どの入力でもテストが通る」という仕様に変換し、コンパイル済みのRISC-V命令とLinuxプロセスの形式意味論から証明課題を生成しました。ClaudeがRocqの証明コードを書き、Rocqカーネルが仕様を満たすかを機械的に検査するため、開発者が約1億8000万行の証明を手作業で読む必要はありません。

証明は中央値1万8000命令のバイナリに対し、典型例で約60万行に達しました。証明を進める過程でClaudeは数百件の不具合を検出し、通常のファザーが届きにくい約20MBの特殊入力で起きる境界外書き込みや、64MB入力を要する境界外読み取りなどを見つけました。

一方、証明生成には数億トークンを要する場合があり、費用対効果の改善が普及の条件です。36件の小規模課題ではOpus 5.5がOpus 5より約40％少ないトークンで半数を証明し、証明を共有したエージェントは単独作業より17％少ないトークンで済みました。

ただし、今回の保証は固定メモリーで動く単一スレッドの静的RISC-Vバイナリなどを前提とし、一般的なx86やARM、動的リンク環境を直接覆いません。また、64MB未満の入力と一部のファズテスト項目が対象で、仕様やCPU・OSモデルが現実とずれていれば不具合は残ります。形式検証は「完全にバグがない」という宣言ではなく、明示した仕様と前提の範囲で安全性を機械検査できる手段です。