重要ポイント
- Anthropicが2026年10月22日、Claudeを使った大規模な「形式的検証」の研究結果を発表
- 検証対象はGoogle「OSS-Fuzz」由来のオープンソースライブラリ123個、239個のエントリーポイント
- Claudeが書いた証明はRocq(旧Coq)という検証系でチェックし、総量は約1億8000万行に達した
- 証明の過程で数百件のバグを発見・修正。libexpatの既知の脆弱性(CVE-2026-56132)も再発見
- 対象はRISC-V・Linux・musl libc・シングルスレッドの静的バイナリに限定され、x86やARM環境は含まない
概要
Anthropicは2026年10月22日、形式的検証を専門とするスタートアップ「Theorem」と共同で、AIモデルのClaudeを使ってソフトウェアの安全性を数学的に証明する研究結果を発表しました。対象はGoogleの脆弱性発見プロジェクト「OSS-Fuzz」に登録されている123個のオープンソースライブラリで、合わせて239カ所の関数(エントリーポイント)について、特定の条件下では異常終了(クラッシュ)しないことを証明したとしています。
形式的検証は、航空機の制御ソフトウェアなど極めて高い信頼性が求められる分野でしか使われてこなかった、手間とコストのかかる手法です。Anthropicはこの研究によって、AIの力を借りればより広い範囲のソフトウェアに形式的検証を適用できる可能性を示したとしています。
詳細
どんな手法か
今回の手法は、各ライブラリにすでに用意されていた「ファズテスト」(ランダムな入力を与えて異常動作を探すテスト)の入口を、コンパイル後のバイナリコードに対する仕様(証明すべき条件)に書き換えるところから始まります。その仕様に対してClaudeが証明を書き、数学的な証明の正しさを検証する「Rocq(ロック、旧名Coq)」というソフトウェアがそれをチェックする、という流れです。生成された証明の総量はRocqのコードで約1億8000万行にのぼったとされています。
証明の対象と条件
証明の対象は、RISC-VというCPUアーキテクチャ上で、Linuxと軽量なCライブラリ「musl libc」を使い、シングルスレッドで動く静的バイナリに限定されています。さらに、与える入力データのサイズも64メガバイト未満という条件がついています。つまり、世の中で広く使われているx86やARMのCPU、glibcを使った環境での動作を直接保証するものではありません。Anthropic自身も発表の中で「『形式的に検証された』ことは『バグがない』ことを意味しない」と明確に注意を促しています。
見つかったバグ
証明を書く過程で、Claudeは数百件のバグを見つけて修正したとしています。例として、ある展開(decompress)処理でカウンターの値が0未満になり、本来許されない範囲への書き込みが発生する不具合が挙げられています。また、XML処理ライブラリ「libexpat」では、2026年に公表された既知の脆弱性CVE-2026-56132を、この検証作業の中で独立に再発見したとしています。ほかにも、ファイルへのアクセス制限機能が常には効いていないという論理上の不具合も見つかったとされています。
今後の提供
Anthropicは、生成した証明の一部と、RISC-VやLinuxの動作を記述したモデルを公開するとしています。また、協業先のTheoremは、今回の検証の仕組みを他のオープンソースプロジェクトにも使えるようにし、使用したClaude向けのスキルも公開するとしています。
