Claudeが120超のソフトで欠陥ゼロを数学的に証明、AIで検証を自動化

米Anthropicは米Theoremと共同で、AIモデル「Claude」を活用してオープンソースソフトウェアの安全性を数学的に証明する「形式検証」を大規模に実施したと発表した。123種類のライブラリを対象に、特定の条件下でプログラムが異常終了（クラッシュ）しないことを機械語レベルで証明したとしている。

ソフトウェアの欠陥（バグ）はサイバー攻撃の標的となりやすく、世界中で数十億台の機器に導入されているLinuxカーネルでも1,000件以上の脆弱性が公開されるなど、従来のテスト手法では見落としを防ぎきれない課題がある。コードが仕様通りに動作することを数学的に証明する形式検証は欠陥を完全に排除する手段として知られていたが、極めて高い専門性と労力を必要とした。例えば「seL4」基本ソフト（OS）では、開発に2人年を要したのに対し、形式検証には20人年がかかり、エアバスの航空電子機器など極めて重要な用途に適用が限られていた。

今回の取り組みでは、Googleの「OSS-Fuzz」基盤にあるCおよびC++言語などのプログラムを対象に、テストケースを「64メガバイト未満のあらゆる入力でクラッシュしない」という仕様に自動変換した。Theoremが提供するRISC-V命令とLinuxプロセスの動作モデルを使い、コンパイル後の機械語を数学的モデルへ変換した上でClaudeに証明を作成させた。その結果、123ライブラリの239カ所のエントリポイントで安全性の証明に成功した。生成された証明コードは証明支援系「Rocq」で合計約1億8,000万行に達し、中央値で1万8,000行のRISC-V命令を持つバイナリに対し、約60万行の証明コードが出力された。正しさはRocqによって機械的に検証されるため、人間が証明コードを精査する必要はない。

検証の過程でClaudeは、何兆回もの自動テストをすり抜けてきた長年のバグを自ら発見し、修正パッチを当てた上で証明を完了させた。発見された問題には、約20メガバイトの特殊な入力でのみ生じるメモリの不正書き込みや、64メガバイトの入力と2ギガバイト超のメモリを要する不具合、既知の脆弱性（CVE-2026-56132）の再発見などが含まれる。両社は今回の成果物の一部を公開したほか、Theoremは他のオープンソースプロジェクト向けに検証パイプラインを提供し、開発者が自身のコードを検証できるようにするClaude向け機能も提供するとしている。