Anthropicは、Claudeがオープンソースライブラリでセキュリティ特性を証明した 123 述べています

Anthropicは、自社のClaudeモデルが123オープンソースライブラリのコンパイルされたコードのセキュリティ特性の形式的証明を生成できたと述べており、これは正式なソフトウェア検証をはるかに大規模に実用化するための一歩と同社は説明しています。2026年10月22日に発表された研究投稿で、Anthropicはこの研究が長年気づかれてこなかったバグも明らかにしたと述べています。

証拠と背景

Anthropicによると、Claudeはプロジェクトのモデル条件下で123ライブラリ間の239エントリポイントがMB未満の入力でクラッシュしないことを証明しました64。同社は証明をRISC-Vバイナリのアセンブリコードレベルで適用し、RISC-VやLinuxのプロセス挙動にはTheoremの形式意味論を用いています。Anthropicは、この取り組みがGoogleのOSS-Fuzzイニシアチブのライブラリを含む実世界のオープンソースソフトウェアをカバーしており、同社の知る限り、アセンブリコードレベルで本番ソフトウェアに形式的検証を適用するためにAIを大規模に活用した初の例であると述べています。

同社は、証明は数週間にわたって生成され、Claudeはプロセス中に遭遇したバグも修正したと述べています。挙げられた例には、まれな20 MB入力レイアウトによる境界外書き込み、64 MB入力と2 GB以上のメモリを必要とする画像デコーダの境界外読み取り、二ファイルハンドル間の特定の呼び出しシーケンスに関連したクラッシュ、libexpatでのCVE-2026-56132再発見などが含まれます。Anthropicはまた、ファイルアクセス制限機能が常に適用されていないケースを含む、ソフトウェアがクラッシュしなかった論理バグ一発見されたと述べています。

同社は、証明は条件付きであり、ソフトウェアがバグなしであることを意味しないと述べています。同社の制限セクションでは、保証はRISC-V Linux上で動作する固定メモリ予算を持つシングルスレッドの静的バイナリを含むモデル化された仮定に依存しており、すべてのエントリーポイントやソフトウェアの本番環境での使用方法を網羅しているわけではないと述べています。Anthropicは、残りの不確実性は信頼できるコンポーネント、すなわちRISC-VとLinuxの意味論、定理文、Rocq証明チェッカーに集中していると述べています。

なぜ重要なのか

Anthropicは、LLMが形式検証のコストを削減できるという証拠としてこの研究を位置づけました。形式検証はこれまで高度に専門的な努力を必要とし、通常はミッションクリティカルなシステムに限定されてきました。投稿によると、より大きなモデルは一部の検証タスクでトークン数が少なくて済み、共有証明コンポーネントは関連プロジェクト間の重複を減らしました。同社はまた、証明の一部を公開する計画であり、Theoremは他のオープンソースプロジェクトにも同様のパイプラインを提供する予定だと述べています。

この研究は、形式検証がテストを補完するのではなく、代替するのではなく補完できることを示す業界全体の研究と一致しています。しかしAnthropic自身が指摘するように、証明の価値は仕様や機械モデルが現実に合致するかどうかに依存しており、多くの展開前提は検証済みの主張の範囲外に残っています。