Anthropic、Claudeを使って123のOSS-FuzzライブラリをRISC-Vアセンブリレベルで形式検証

AnthropicとTheoremが発表した内容

Anthropicは、検証企業Theoremと協力し、Claudeがこれまで実用的ではなかった規模で形式ソフトウェア証明を書けることを発表しました。チームはClaudeを使って、100以上の実世界のオープンソースライブラリのコンパイル済みRISC-Vアセンブリ上で直接セキュリティ特性を証明しました。具体的には、123のOSS-Fuzzライブラリにわたる239のファジングエントリポイントです。Anthropicはこの結果を次のように説明しています。「私たちの知る限り、これはAIを使ってアセンブリコードレベルで本番ソフトウェアに形式検証を適用する初めての大規模な取り組みです。」

証明された特性は「バグがない」というものより狭く、Anthropicはその点を明確にしています。Claudeは、カバーされた各プログラムが、64MB未満のすべての入力と、モデル化されたすべてのLinuxオペレーティングシステムの応答およびメモリレイアウトに対して、メモリ安全性エラーを引き起こさず、アサーションの失敗もなく、常に正常に終了することを証明しました。これらの証明は、プログラムがRISC-V CPU上でLinuxを実行し、固定メモリ予算でシングルスレッドの静的バイナリとして実行されることを前提としています。

OSS-Fuzz検証の主要な数字

123の異なるOSS-Fuzzライブラリにわたって、239のファジングエントリポイントが証明されました。
合計で約1億8000万行のRocq証明。
典型的な証明は約60万行で、中央値で18,000のRISC-V命令を含むバイナリをカバーしています。
証明を生成するのに数週間の作業。

形式検証は歴史的に、計算ではなく専門家の時間が高価でした。Anthropicは、検証済みオペレーティングシステムカーネルであるseL4を例に挙げています。実装には2人年かかりましたが、形式検証には20人年かかりました。このコストプロファイルが、検証がエアバスのアビオニクスなどのミッションクリティカルなコードに限定されてきた理由です。この研究の主張は、LLM生成の証明がその計算を変えるというものです。

ファズテストが形式仕様に変換される方法

方法論の中核は、手動で仕様を書くことを避けることです。ほとんどのプログラムでは、包括的で曖昧さのない仕様が難しい部分です。Anthropicが問うように、テキストエディタやウェブブラウザが「正しい」とはどういう意味でしょうか？代わりに、チームは「この既存のテストスイートは常にパスする」というルールを、コンパイルされたRISC-V命令に対する形式仕様としてエンコードし、Linux上で任意のRISC-Vコンパイルバイナリを実行することの一般的なモデルを使用します。

具体的には、パイプラインは4つの段階で機能します。

ライブラリとその既存のファズテストがRISC-V実行可能ファイルにコンパイルされます。OSS-FuzzはCおよびC++プログラムにAddressSanitizer（ASan）を自動的に計測し、不適切なメモリアクセスをクラッシュさせます。
Theoremの形式RISC-V命令およびLinuxプロセスセマンティクスが、マシンコードを数学モデルに変換します。
Claudeは、生成された仕様が成立するというRocq証明を書きます。
Rocq証明チェッカーが、仕様に対して証明を機械的に検証します。

仕様は、ファズテストが64MB未満の任意の入力に対してクラッシュしないことを述べています。証明が成立すれば、そのエントリポイントのファジングは何も見つけることができなくなります。ASanがリンクされている間に「クラッシュしない」ことを証明することは、カバーされたパスに対してメモリ安全性も確立します。ASanは範囲外アクセスをクラッシュに変換するからです。

開発者が実際に信頼しなければならないもの

Anthropicは、生成された証明コードのほぼすべてが人間のレビューを必要としないと主張しています。Rocq証明チェッカーが、仕様に対する証明の正しさを強制するからです。残る信頼される成果物は小さく、列挙可能です。

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

Anthropicはその結果を明確に述べています。「これはこれらのライブラリにバグがないという意味ではありません。」残りのバグは、これらの信頼されるコンポーネント内に存在するか、証明の範囲外にあります。これらのコンポーネントを強化することは簡単ではありませんが、Anthropicは、証明でカバーされるすべての行を監査するよりもはるかに扱いやすいと主張しています。また、コードとは異なり、信頼される基盤は、より多くのプロジェクトが検証されるにつれて成長しません。

何年ものファジングが見逃したバグが発見された

証明を試みることで数百のバグが表面化し、Claudeはそれらを自律的にパッチすることが許可されました。コードを修正し、パッチされたコードから仕様を再生成し、Claudeは新しい仕様を証明しました。これは重要でした。なぜなら、多くのバグは従来のファジングの範囲外にあったからです。従来のファジングは通常、約1MBに制限された小さな入力を変異させ、カバレッジガイダンスに依存します。

Anthropicが報告した具体的な例：

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

Anthropicはこの点を要約しています。最終目標である完了したノークラッシュ証明に到達しない場合でも、試み自体が修正が必要な実際のバグを生み出します。

メモリ安全性を超えた特性の証明

ファズテストが決してクラッシュしないことを証明することは、聞こえるよりも強力です。なぜなら、実世界のファズテストは高レベルの特性を頻繁にエンコードするからです：エンコード-デコードのラウンドトリップ、冪等性、代数法則、差分テスト、自己整合性、またはリファレンス実装との等価性。例えば、LZO圧縮アルゴリズムのファズテストは、入力を圧縮してから解凍すると元に戻ることをアサートします。プロパティが失敗するとプログラムがクラッシュするため、テストが決してクラッシュしないことを証明することは、プロパティ自体を証明することと同等です。

プロパティは、開発者によって述べられなくても、証明の途中で必要になることがあります。cpp-httplibのOSS-Fuzz証明を完了するために、Claudeはstd::setデストラクタでの過度の再帰によるスタックオーバーフローを除外する必要がありました。その再帰の深さはツリーの最大深さによって制限されるため、Claudeはマシンコード上で、libc++の赤黒木再バランスアルゴリズムがツリーの深さを対数的に制限することを証明する必要がありました。

同じレポート内の他の形式検証ケーススタディ

Anthropicは、OSS-Fuzzパイプラインに加えて3つの追加実験を説明しています。

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

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

重要なアプリケーションでのセキュリティ特性。 広く使用されているソフトウェアの単純なセキュリティ特性を検証すると、問題が直接表面化しました：あるアプリケーションでは、10年以上潜伏していた以前は未知のロジックバグ、広く使用されているPDFリーダーでは、1週間で通常1年間に報告されるのと同じ数のセキュリティバグが見つかりました。

コスト、トークン効率、証明の再利用

Anthropicは、コストを現在の主な制限として挙げています：証明は生成に数億トークンを要する可能性があります。改善を期待する理由として2つの傾向が挙げられています。

第一に、新しいモデルはより少ないトークンを必要とします。実際のOSS-Fuzzコードから構築された36の小さな検証タスクで、Opus 5.5はOpus 5よりも約40%少ないトークンでその半分を証明します。各タスクには、5Mトークンの予算で3回の独立したシングルエージェント試行が与えられ、最初の試行が完了したときに証明されたとカウントされました。Anthropicは、モデルが長い検証タスクでトレーニングされるにつれて、この傾向が続くと予想しています。

第二に、証明は再利用できます。証明はソフトウェアと同様に、より小さな証明から再帰的に構築され、より小さな証明はより再利用可能です。エージェントが共有ワークスペースで作業し、互いの証明をコピーした場合、単独で作業するエージェントよりも17%少ないトークンを必要とし、一部のエージェントは以前に単独で失敗した後に成功しました。36タスクの実験全体で、共有ワークスペースのコストは34の完了した証明のうち30で単独平均よりも低く、単独で作業するエージェントはそのうちの2つを完了できませんでした。

同じ効果がOSS-Fuzzの取り組みで大規模に現れました。証明の多くは、すべてのプログラムに含まれるコード、特にCランタイムとAddressSanitizerの初期化に関するものであるため、無関係なプログラムは大幅に重複する証明を持つことになります。エージェントチームは完了した証明をコピーして自分のプログラムに適応させました。libcups、freerdp、libzmqの公開比較では、共有部分はほとんど新しいコードを獲得しませんでした。

Anthropicはこれを、Leanの形式数学の共有ライブラリであるMathlibと比較しています。Mathlibは、各新しい証明が既存の作業に基づいて構築されるため、700人以上によって貢献された約30万の定理に成長しました。同社はOSS-Fuzz証明のサブセットをリリースし、未パッチのバグを明らかにする可能性のある証明は保留しました。

リリースされた成果物と作業の再現方法

証明：サブセットがgithub.com/theorem-labs/oss-verify-proofsで公開されており、パッチを必要としなかったファズテストの完全なRocq証明と、証明できなかったファズテストの仕様が含まれています。
セマンティクス：信頼されるモデルとして使用されたRISC-VおよびLinuxプロセスセマンティクスが、github.com/theorem-labs/rocq-linux-process-semanticsで公開されています。
ツール：Theoremは、開発者が自分のコードをオンボードするのに役立つClaudeスキルを公開し、他のオープンソースプロジェクトに対して同じパイプラインを実行することを提供しています。
完全な付録：より長いPDF付録には、追加のケーススタディと外部専門家による証明の評価が含まれています。

LLM支援形式検証の明示された制限

Anthropicは、「形式検証」が「バグがない」と同じではない理由についてのセクションを割いており、3つの異なるギャップを特定しています。

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

主張が重要ですべてをカバーしていない可能性がある。 ASanはすべてのメモリ安全性バグを検出するわけではなく、各ライブラリのすべてのエントリポイントが検証されたわけでもありません。すべてのエントリポイントを検証しても、特にデッドコードがある場合、ライブラリ全体をカバーすることはできません。実際のプログラムはライブラリを誤用して呼び出し側でメモリ破損を引き起こす可能性もあります。このギャップを埋めるには、各パブリック関数について呼び出し側が何をしなければならないかを指定し、呼び出し側がそれに従うことを要求する必要があります。

仕様が現実と一致しない可能性がある。 証明チェッカーは、仕様が現実世界に対応するかどうかを教えてくれません。Anthropicは次のように書いています。「Claudeは、コンパイルされたプログラムの動作が形式仕様の要件を満たすことを示す証明を書くことができます（外部の証明チェッカーによって検証されます）。しかし、証明チェッカーは仕様が現実と一致するかどうかを教えてくれません。」検証されたコードにバグが現れるとき、それは仕様または想定されたマシンセマンティクスが現実から逸脱しているためです。これは少なくともどこを見るべきかを教えてくれます。

Hacker Newsの議論が追加したもの

議論で最も再掲された批判は、検証は仕様と同じくらいしか良くないというものでした。あるコメント投稿者は、はしごをビジョン、青写真、検査として要約しました：「この研究は検査をほぼ完璧にします。しかし、検査は青写真だけをチェックし、私たちのビジョンはチェックしません。だから、間違った青写真から建てられた家は完璧な検査に合格することができます。」関連するコメントは、誰がモデルが検証されているプログラムを忠実に表現していると確信できるのかと尋ねました。「実際にはあなたのプログラムではないものを証明した可能性は十分にありますか？」そして別のコメントはもっと率直に言いました：「現実の形式仕様を想像してみてください！」

第二のテーマは、標準的な検証と妥当性確認の区別が依然として適用されるというものでした。あるコメント投稿者はIEEEの用語でそれを説明しました：検証は「製品を正しく構築しているか？」を尋ね、妥当性確認は「正しい製品を構築しているか？」を尋ねます。「数学的に完璧なコードを書いて、間違った問題を非常に効率的に解決することができます。」

第三のテーマは、予測される能力の壁でした。あるコメント投稿者は、レポート自体の付録を引用しました。そこでは、エージェントが冗長な証明スタイルをより複雑なプログラムにスケールできるかどうかが問われ、「他のエージェントベースの検証プロジェクト、例えばMachCSLからの経験は、答えがノーかもしれないことを示唆しています：エージェントは冗長な証明スタイルで複雑さの壁にぶつかります。」同じコメント投稿者は、形式検証がLLM推論の有用なリトマス試験であると主張しました。なぜなら、これらのシステムは必ずしもモデルの分布上にあるとは限らないからです。これは、LLMが人間が生成した数学のフロンティアのすぐ先で停滞するという「凸包」仮説に信憑性を与えます。

スレッドの実践者は自分の成功を報告しました。ある人は、RustとCの両方をLeanに変換するコンパイラを構築し、LLMに行動等価性を証明させ、シングルスレッド実行でコードの約12%をカバーしたと言いました。これは約70,000行のCで、浮動小数点の動作がプラットフォーム間で異なるなどの非常に小さな違いを見つけました。別の人は、SIMDまたはCUDAで関数を高速化するPRを開き、「PRに元の実装と行動的に等価であるというRocq証明があるため」自信を持ってマージしたエージェントについて説明しました。3人目は、Codexを使用して認可システムのAlloyモデルを構築し、その後サーバーを数時間レッドチームして特権昇格を生成しなかったと報告しました。

懐疑論は、技術的な限界ではなく組織的なインセンティブにも焦点を当てました。あるコメント投稿者は採用が続くとは疑っていました：「ソフトウェアにおけるLLMの採用はこれまで主にベストプラクティスを捨てることだったので、それが検証の拡大につながるとは懐疑的です。」と、幹部が短い労働週を予測することに例えました。別の人は、怠惰が本当のリスクであると警告しました。コードレビューをスキップして形式検証を雰囲気でコーディングすることは依然として問題を引き起こし、「完璧は善の敵です。」

数人のコメント投稿者は労働への影響を直接提起し、ある人はレポートの著者が、証明が形式成果物と一致しないもっともらしい論文というLeanの類似性を考慮したかどうか尋ねました。これは以前のOpenAI Leanの研究を指しています。他の人はコードから証明へのワークフローの詳細を求め、少なくとも1人は、Claudeは指示されない限り形式検証に手を伸ばさないと指摘しました。

これがソフトウェアの構築方法にとって重要な理由

Anthropicの結論は、完成品の主張ではなく軌道の主張です：形式検証は、歴史的に最も安全性が重要なコードでの特注の専門家が作成した保証にのみ実用的でしたが、今日のファジングと同様に、ほとんどの本番ソフトウェアにとって実用的になり、言語設計と開発ワークフローの変更とともに、後付けから組み込みに移行します。同社は、あまり能力のないモデルで形式検証を試みてうまくいかなかった開発者に、もう一度試すことを明示的に奨励しています。

レポートはまた、既存のソフトウェア基盤の戦略を概説しています：コードベースを別の言語で書き直す必要がないように、一般的な仕様でバイナリレベルで検証し、パッケージ粒度で証明を再利用して、各依存関係が一度検証されるようにします。依存関係はべき乗則に従うため、共有ライブラリの小さなセットを証明すること（TheoremのロードマップはNixエコシステム内のglibc、OpenSSL、cURLを挙げています）で、ソフトウェアの大部分の検証が可能になります。