この記事のポイント
- AnthropicがClaudeを使い、OSSの123ライブラリ・239か所を形式検証しクラッシュしないことを証明した
- 検証で見つかった数百件のバグは、仕様の再生成から修正までClaude自身が一貫して対応した
- 「形式検証済み=バグゼロ」ではなく、仕様と実環境の差など残る限界も公式に明記されている
Anthropicのフロンティア・レッドチームが2026年10月22日、Claudeに大規模なソフトウェア検証を任せた研究成果を公式ブログで公開しました。オープンソースの脆弱性発見ツール「OSS-Fuzz」に登録された123個のライブラリを対象に、AIにコードの安全性そのものを証明させた今回の試みを、企業のAI活用という観点から整理します。
「クラッシュしないこと」を数学的に証明する、とはどういうことか
記事のテーマである形式検証とは、ひとことで言うと「定めた前提条件の下で、このプログラムは特定の不具合を起こさない」と数学的に証明する手法です。テストのように一部のケースを確認するのではなく、設定した範囲の入力すべてに対して成り立つことを証明します。精度は高い一方、従来は専門知識と膨大な工数が必要で、OSのセキュリティ基盤として知られる「seL4」カーネルは実装に2人年、検証にはその10倍の20人年を要したといいます。
Anthropicは、この作業を形式検証ツールを手がけるTheorem社と共同で、Claudeにやらせました。対象はOSS-Fuzzに登録された123個のオープンソースライブラリ・239個の呼び出し窓口(エントリポイント)で、証明の総量は約1億8,000万行(証明記述言語Rocqによる)。ここまでの作業を数週間で終えたとされています。証明した内容は「64MB未満のどんな入力を与えても、メモリ安全性の違反やクラッシュが起きない」こと(前提はシングルスレッドの静的RISC-Vバイナリ、Linux上での動作)です。
見つかった数百件のバグも、直すのはClaude自身
検証の過程では数百件のバグが見つかりました。注目したいのは直し方です。Claudeがパッチを当てると仕様が自動で再生成され、Claude自身がもう一度証明をやり直す、というサイクルを人の介入なしで回したといいます。具体例として、展開処理(decompressor)でカウンタの計算がずれて領域外に書き込んでしまう不具合や、画像デコーダが範囲外のメモリを読み取ってしまう不具合、既知の脆弱性(CVE-2026-56132)に相当する問題の再発見などが紹介されています。証明が不正に通りやすくなる「ズル」(報酬ハッキング)を防ぐため、パッチの変更範囲が小さいことも別途証明させ、ログを監査する仕組みも組み込んだとのことです。
ただし、Anthropicは「形式検証済み=バグゼロ」ではないと明記しています(証明は仕様どおりに動くことしか保証せず、その仕様自体が実機の挙動と完全に一致しているかは別問題であるため)。今回の証明も、実際に多いx86やARM・動的リンクの環境ではなく、静的なRISC-Vバイナリが対象である点や、呼び出し側の誤用までは防げない点など、残る限界も併せて公開されています。
まとめ
今回の成果は、数週間で123ライブラリの特定条件を検証できたという研究報告です。先に紹介したseL4の20人年とは対象も検証範囲も異なるため、作業時間を直接比較することはできません。Anthropicは今後、安全が特に重要な分野だけでなく、ほぼすべての本番ソフトウェアで形式検証が実用的になると見通しています。社内で使っているOSSの依存ライブラリの安全性をどう確認するか、今後の判断材料として知っておく価値があるでしょう。AIがソフトウェアの不具合を見つけて直す動きは他にも広がっており、PHPの重大な脆弱性をAIが発見・修正した実例や、Anthropicがオープンソースを守るために別途進めている「Cyber Mission」という施策も、合わせて読むと流れがつかみやすくなります。
※2026年10月時点の情報です。
