クロード氏、オープンソース ソフトウェアの初の大規模 AI 正式検証で 1 億 8,000 万行の数学的証明を作成

完全なレポート

Anthropic は 10 月 22 日、公式研究ページで、ソフトウェア検証会社 Theorem と協力して、Claude が Google の OSS-Fuzz から抽出された 123 の実際のオープンソース ライブラリにわたって、239 のプログラム エントリ ポイントをカバーする RISC-V アセンブリ レベルのセキュリティ プロパティを正式に検証したと発表しました。同社はこれを「AIを使用してアセンブリコードレベルで本番ソフトウェアに形式的検証を適用する初の大規模な取り組み」と呼んでいる。

その規模は驚くべきものです。Rocq の証明は約 1 億 8,000 万行、典型的な証明は約 60 万行に達し、中央値の長さ 18,000 RISC-V 命令のバイナリをカバーしており、すべてが数週間で完了します。 Rocq カーネルは各証明を独立してチェックするため、手動で行ごとにレビューする必要はありません。

このメソッドは、既存のファズ テストを数学的仕様に変換します。64 MB 未満の入力の場合、Linux 上のシングルスレッドの静的にリンクされた RISC-V バイナリは、メモリ安全性違反なく常に正常に終了する必要があります。 Claude が途中でバグを疑ったとき、コードに直接パッチを当て、新しい仕様を再証明しました。

その過程で何百ものバグが表面化しました。これには、境界外書き込みにつながるデコンプレッサーのコピーでのカウンター アンダーフロー (まれなレイアウトで 20 MB までの入力によってのみトリガー可能)、画像デコーダーでの境界外読み取り、libexpat での CVE-2026-56132 の再発見などが含まれます。いくつかの脆弱性は長年にわたって潜んでいました。

Anthropic はその限界自体を認めています。正式な検証に合格したからといって、バグがないことを意味するわけではありません。証明はシングルスレッドの静的 RISC-V バイナリのみをカバーしており、ほとんどのコードは実際には x86/ARM 上で実行されます。 Theoremは、独立した検証のためにGitHubで証明のサブセットを公開しており、他のオープンソースプロジェクトでも同じパイプラインを実行すると述べている。

副次的な結果も注目に値します。Linux カーネルの zlib 実装は、x86 バイナリ レベルで RFC 1950 に準拠していることが証明され、Rust で書かれた Python インタプリタの大規模なサブセットは、170 万以上のランダム化されたプログラムの 99.95% で CPython の動作と一致しました。