AnthropicのLLM形式検証：ClaudeがRISC-Vアセンブリレベルで123のOSS-Fuzzライブラリのクラッシュなし特性を証明

Anthropicとその協力者であるTheoremは、Claudeがソースコードではなくコンパイル済みのRISC-Vアセンブリ上で直接、123の実世界のオープンソースライブラリに対してクラッシュなしのセキュリティ特性を自律的に証明したと報告しています。Anthropicはこれを、アセンブリコードレベルで本番ソフトウェアにAI駆動の形式検証を適用した初の大規模な取り組みと呼び、その証明は何年ものファジングが見逃していたバグも表面化させたと述べています。

発表された内容

中心となる主張は、LLM支援による形式検証が実用性の閾値を超えたということです。確率的にクラッシュを探すファジングにのみ依存するのではなく、Claudeは定義された境界内の任意の入力に対して、特定のコンパイル済みプログラムが決してクラッシュしないという数学的証明を生成しました。

具体的には、AnthropicはClaudeが100以上の実世界のオープンソースライブラリでRISC-Vアセンブリレベルでの有用なセキュリティ特性を証明したと報告しています。その取り組み全体で、ClaudeはGoogleのOSS-Fuzzイニシアチブからの123のライブラリにわたる239のエントリポイントの証明を完了しました。この作業はTheoremと協力して行われ、Theoremは機械コードを数学的モデルに変換するために使用されるRISC-V命令およびLinuxプロセスセマンティクスを提供しました。

Anthropicはその動機を明確に示しています：存在する中で最もテストされたソフトウェアの1つであるLinuxカーネルでは、最近1,000を超える脆弱性が開示されており、フロンティアモデルは無害に見えるバグを連鎖させて重大なエクスプロイトにする能力がますます高まっています。LLMが大規模にバグを見つけることができるなら、防御側はバグの存在をテストするだけでなく、その不在を証明できる技術が必要であるという議論です。

Claudeを使用して、100以上の実世界のオープンソースソフトウェアライブラリでアセンブリコードレベル（RISC-V）のセキュリティ特性を証明しました。私たちの知る限り、これはAIを使用してアセンブリコードレベルで本番ソフトウェアに形式検証を適用した初の大規模な取り組みです。

パイプラインがファズテストを証明に変える方法

このパイプラインは、開発者がすでに行った作業を再利用します。OSS-Fuzzプロジェクトには、プロパティが違反されたときにプログラムをクラッシュさせる開発者作成のエントリポイントが数千含まれています（例：アサーションの失敗やAddressSanitizerによって検出された不正なメモリアクセス）。これらのエントリポイントと既存のファズテストは、RISC-V実行可能ファイルにコンパイルされます。

その実行可能ファイルは、TheoremのRISC-VおよびLinuxセマンティクスと望ましいクラッシュなしプロパティと組み合わせることで、証明が満たさなければならない仕様を機械的に生成します。次にClaudeが証明を書き、Rocq証明チェッカーがその仕様に対して検証します。証明の試みが失敗した場合、その失敗は実際のバグを指し示します。Claudeはコードをパッチし、パッチされたコードから仕様が再生成され、サイクルが繰り返されます。

証明された正確なプロパティは狭いですが意味があります：これらのプログラムは、64 MB未満のすべての入力、およびモデル化されたすべてのLinux OS応答とメモリレイアウトに対して、メモリ安全性エラーやアサーションの失敗を引き起こさずに常に正常に終了します。

証明は、プログラムがLinux上で動作するRISC-V CPU上で固定メモリ予算を持つシングルスレッドの静的バイナリとして実行されるという前提の下で成立します。Anthropicは、範囲を拡大するには、より多くのアセンブリアーキテクチャや他のオペレーティングシステムプロセスのセマンティクスを標準化することが含まれると述べています。

証明作業の規模

数字は、これが手書きの検証とは異なる体制であることを示す見出しの証拠です。

123のOSS-Fuzzライブラリにわたって239のエントリポイントが証明されました
合計で約1億8000万行のRocq証明が生成されました
典型的な証明は約60万行です
証明でカバーされるバイナリの中央値は約18,000のRISC-V命令です
入力境界：64 MB未満のすべての入力
タイムライン：数週間の期間

Anthropicが引き合いに出す歴史的な比較は、seL4オペレーティングシステムカーネルです。これは実装に2人年かかりましたが、形式検証には20人年かかりました。この比率が、形式検証がエアバスのアビオニクスコードなどのミッションクリティカルな領域に限定されてきた理由です。

開発者がまだ信頼しなければならないもの

1億8000万行の証明コードのほとんどすべては、Rocq証明チェッカーが検証するため、手動レビューは必要ありません。Anthropicは、開発者が信頼しなければならない正確に3つの成果物をリストアップしています：

RISC-VおよびLinuxプロセスの形式的モデル
証明された正確な定理ステートメント
Rocq証明チェッカー自体

これが重要な構造的議論です。信頼できるコンピューティングベースは、検証されたプロジェクトの数に応じて増大しません。Anthropicは、これはライブラリにバグが含まれていないことを意味するものではないと明示的に警告しています。それは、残っているバグがそれらの信頼できる成果物の中にあるか、証明の範囲外にあることを意味します。Rocq、RISC-Vセマンティクス、およびLinuxセマンティクスを強化することは実際の作業ですが、プロジェクトごとの負担ではなく、限定されたタスクです。

Claudeが証明を書いている間に見つけたバグ

証明を試みることは、それ自体がバグ発見プロセスであることが判明しました。Anthropicは、この取り組みで数百のバグを発見し、その多くはファザーが決して見つける可能性が低いものであると報告しています。その理由は機械的です：ファザーは小さな入力を変異させ、通常は1 MBに制限され、コードカバレッジに依存して検索をガイドします。

Anthropicが説明する具体的な例：

ライブラリのデコンプレッサのコピーにおけるカウンタアンダーフローで、約20 MBの入力と1つのまれな特定のレイアウトでのみ到達可能な範囲外書き込みにつながりました。
画像デコーダーでの範囲外読み取りで、64 MBの入力と2 GBを超えるメモリが必要でした。
別のライブラリでの範囲外読み取りで、同じファイルへの2つのハンドルにわたる特定の呼び出しシーケンスが必要でした。
libexpatでのCVE-2026-56132の再発見で、深くネストされた入力が必要でした。
クラッシュのない純粋なロジックバグ：あるライブラリのメモリ安全性を証明しているときに、Claudeはアプリケーションがロードできるファイルを制限する機能が常に強制されるわけではないことに気付きました。

バグが現れるたびに人間のために停止するのを避けるために、AnthropicはClaudeが同じループの一部として見つけたバグをパッチすることを許可しました。

メモリ安全性以上の証明

ファズテストが決してクラッシュしないことを証明することは、聞こえるよりも強力です。なぜなら、実際のファズテストはメモリチェックだけでなく高レベルのプロパティをエンコードするからです。Anthropicは、エンコード-デコードのラウンドトリップ、冪等性、代数法則、差分テスト、自己整合性、および参照実装との等価性を一般的な例として挙げています。たとえば、LZO圧縮アルゴリズムのファズテストは、入力の圧縮とその後の解凍が元のものを返すことをアサートします。失敗はプログラムをクラッシュさせるため、テストが決してクラッシュしないことを証明することは、プロパティ自体を証明することと同等です。

時には、必要な義務が開発者の意図を超えることがあります。cpp-httplibのOSS-Fuzz証明を完了するために、Claudeはstd::setデストラクタでの過度の再帰によって引き起こされるスタックオーバーフローを排除する必要がありました。その再帰の深さはツリーの最大深さによって制限されるため、Claudeはマシンコードレベルで、libc++の赤黒木再バランスアルゴリズムがツリーの深さを対数的に制限されたままに保つことを証明する必要がありました。

その他の形式検証ケーススタディ

Anthropicは、OSS-Fuzzのファズテストから証明へのパイプライン以外にもいくつかの追加実験について説明しています。

zlibとRFC 1950。 Claudeは、zlib圧縮ファイル形式を定義する文書であるRFC 1950の形式的仕様を作成し、Linuxカーネル内のzlib実装がその仕様を正しく実装していることを証明しました。RISC-Vの作業とは異なり、この証明はClaudeが生成し、徹底的にテストされたx86 ISAの形式的セマンティクスを使用して、x86コンパイル済みバイナリ上で直接実行されました。このプロセスは他の半ダースの広く使用されているライブラリでも繰り返され、上流に報告されているコーナーケースで軽微で悪用不可能なバグが見つかりました。Anthropicは2つの結論を導き出しています：これらの非常にテストされたコードベースはすでにほぼ完全に正しく、エンドツーエンドの正確性プロパティは実際の既存のコードベースについて証明できるということです。

RustでのPythonインタプリタ。 ClaudeはRustでPythonの大きなサブセットのインタプリタを開発し、Verus検証ツールを使用して、学術論文で概説されているCPythonセマンティクスに準拠していることを証明しました。170万を超えるランダムに生成されたPythonプログラムでの経験的テストでは、テストの99.95%でCPythonと同一の動作が見られ、残りの違いは驚くべきことではない既知のコーナーケースでした。

重要なアプリケーション。 単純なセキュリティプロパティの形式検証の試みは、いくつかの広く使用され重要なアプリケーションで問題を表面化させました。あるケースでは、Claudeは10年以上潜伏していた未知のロジックバグを発見しました。広く使用されているPDFリーダーを検証する取り組みの中で、Anthropicは1週間で通常1年間に報告されるのと同じ数のセキュリティバグを見つけたと報告しています。

コスト：トークン使用量とそれがなぜ下がるべきか

Anthropicはトークンコストを重要な制限として特定しています。証明の生成には数億トークンかかる可能性があり、これらの方法がソフトウェアエコシステム全体に到達するためにはコスト効率が重要です。2つの測定された傾向は、コストが下がることを示唆しています。

1つ目はモデルの改善です。Anthropicは実際のOSS-Fuzzコードから36の小さな検証タスクを構築しました。Opus 5.5は、Opus 5よりも約40%少ないトークンでそれらの半分を証明します。各タスクには、5Mトークンの予算で3つの独立したシングルエージェントの試行が与えられ、最初の試行が完了したときに証明されたとカウントされます。

2つ目は証明の再利用です。エージェントが互いの証明をコピーできる共有ワークスペースを与えられた場合、単独で作業するよりも17%少ないトークンで済み、ソロの試行が以前失敗したタスクで成功したエージェントもいました。

同じ効果がOSS-Fuzzの取り組みで大規模に現れました。証明のほとんどは、すべてのプログラムに含まれるコード、特にCランタイムとAddressSanitizerの初期化に関するものであるため、非常に異なるプログラムでも最終的にはかなり重複する証明になります。エージェントチームは別のチームの完成した証明をコピーして適応させました。libcups、freerdp、libzmqの公開された比較では、各証明は同一に保たれた量、軽く編集された量、より多く編集された量、または新しく書かれた量によって分類され、共有部分はほとんど新しいコードを獲得しませんでした。36の共有ワークスペース証明のうち34が完了し、そのうち30は平均的なソロエージェントの試行よりもコストがかかりませんでした。

Anthropicはこのダイナミクスを、Leanの形式数学の共有ライブラリであるMathlibと比較しています。Mathlibは700人以上の貢献者によって提出された約30万の定理に成長しました。これは、各新しい証明が既存の作業に基づいて構築されるためです。

Anthropicが認める制限

この投稿は、形式検証が人々が想定する保証を提供しないことを明確にしています。

「形式検証済み」は「バグなし」を意味しません。 証明チェッカーはプログラムが仕様を満たすことを示すことができますが、仕様が現実と一致するかどうかはわかりません。検証されたコードにバグが現れた場合、仕様または想定されたマシンセマンティクスが現実と異なります。Anthropicは、これは残りのバグを探す場所を示すため、依然として有用であると主張しています。

実際のマシンはモデルが記述しないことを行います。 証明は、musl libcにリンクされたシングルスレッドの静的RISC-Vバイナリをカバーしています。ほとんどの人はこれらのライブラリをx86またはARMでglibcに対して動的リンクで実行します。このギャップを埋めるには、展開されたシステムにより密接に似たシステムモデルが必要です。たとえば、x86の正確なセマンティクスを生成するなどです。

主張は私たちが気にするすべてをカバーしていない可能性があります。 ASanはすべてのメモリ安全性バグを検出するわけではなく、各ライブラリのすべてのエントリポイントが検証されたわけでもありません。すべてのエントリポイントを検証しても、特にデッドコードが存在する場合、ライブラリ全体をカバーすることはできません。実際のプログラムは、呼び出し元のメモリを破壊する方法でライブラリを誤用することもあります。そのギャップを埋めるには、各公開関数について呼び出し元が何をすべきかを指定し、呼び出し元がそれに厳密に従うことが必要です。

リリースされたもの

AnthropicとTheoremは、投稿とともにいくつかの成果物を公開しました：

証明のサブセット（github.com/theorem-labs/oss-verify-proofs）。パッチを必要としなかったファズテストのClaudeの完全なRocq証明と、証明できなかったファズテストの仕様が含まれています。
RISC-VおよびOSセマンティクス（github.com/theorem-labs/rocq-linux-process-semantics）。
開発者が自分のコードの検証を開始するのに役立つClaudeスキル（github.com/theorem-labs/oss-verify）。
他のオープンソースプロジェクトに対して同じパイプラインを実行するというTheoremからの申し出。

Anthropicは、オープンソースソフトウェアの未パッチのバグを明らかにする可能性のある証明を意図的に公開せず、公開されたものの独立した検証を呼びかけています。

これが重要な理由

戦略的な議論は、LLMが脆弱性を見つけて連鎖させる能力が向上するにつれて、テストだけでは不十分な防御になるということです。形式検証は確率ではなく保証を提供し、その歴史的な妨げは証明の価値ではなく、証明を書くコストでした。

Anthropicはまた、ユニットエコノミクスがプログラムではなくパッケージを支持すると主張しています。証明の再利用はパッケージレベルの粒度で機能するため、各依存関係は一度だけ検証される必要があり、依存関係はべき乗則に従います：共有ライブラリの小さなセットを証明することで、下流のソフトウェアの広大な範囲を証明可能にします。glibc、OpenSSL、cURLなどの重要なインフラストラクチャを含むNixエコシステム全体を検証するというTheoremのロードマップは、即時の大規模アプリケーションとして提示されています。

締めくくりの予測は、歴史的に最も安全性が重要なコードでの特注の専門家が作成した保証にのみ実用的だった形式検証が、ほとんどすべての本番ソフトウェアに対して今日のファジングと同じくらい実用的になり、後付けから組み込みに移行するということです。Anthropicは、以前にあまり能力のないモデルで形式検証を試みてうまくいかなかった開発者に、もう一度試すことを明示的に奨励しています。