LLMが大規模な形式的ソフトウェア検証を可能にする

LLMが大規模な形式的ソフトウェア検証を可能にする

Keane Lucas, Aengus Lynch, Luna Tong, Luke Champine, Zygi Straznickas, Dino Distefano, Harshikaa Agrawal
Evyatar Ben Asher, Ava Howell, Sami Jawhar, Chris Rohlf, Nickolai Zeldovich
Nicholas Carlini, Rajashree Agrawal, Jason Gross

ほとんどのソフトウェアにはバグが蔓延しており、AIはそれらを容易に発見し、悪用できるようになりました。サイバー攻撃に対する標準的な防御策はもはや十分ではありません。コードにバグがないことを証明する方法が必要です。形式的ソフトウェア検証は、この保証を提供できますが、歴史的には長年の専門家の努力を必要とし、ほとんどの現実世界のプロジェクトには実用的ではありませんでした。しかし、Theoremとの協力により、状況は変わりました。LLMは現在、大規模に形式的証明を生成でき、検証済みのセキュリティ保証を含む新しいソフトウェア開発ワークフローを可能にします。Claudeを使用し、100以上の現実世界のオープンソースソフトウェアライブラリで、アセンブリコードレベル（RISC-V）のセキュリティプロパティを証明しました。我々の知る限り、これはAIを使用して、本番ソフトウェアにアセンブリコードレベルで形式的検証を適用する最初の試みです。 証明を作成する過程で、Claudeは数兆回のテスト実行にもかかわらず、長年検出を逃れていたバグも発見しました。モデルの能力が向上し続けるにつれて、形式的検証はセキュアなソフトウェア開発の不可欠な一部になると予想されます。

Introduction

成熟し、徹底的にテストされたソフトウェアでさえバグを含んでおり、LLMはそれらを見つけるのがますます得意になっています。Linuxカーネル—今日最もよくテストされているソフトウェアの1つであり、数十億台のデバイスに展開されています—には、最近1,000以上の脆弱性が公開されました。最先端のモデルが、一見無害なバグを連鎖させて重大なエクスプロイトに繋げることができるようになるにつれて、野放しに悪用される前にこれらのバグを検出し修正する技術が必要になります。

理想的には、そのような技術はすべてのバグを見つけて修正し、それ以上バグがないことの証明を提供できるべきです。形式的検証はそのための1つの方法です。形式的検証では、開発者はコードを数学的モデルに変換し、それが定義された一連のセキュリティルールを常に遵守していることを証明しようとします。もし証明に失敗した場合、コードにルールに違反するバグが存在する可能性があり、失敗の性質がバグの可能性を示唆します。このプロセスを繰り返す（毎回失敗の原因を取り除いた後）ことで、最終的にコードがそれらのルールに違反するバグを一切含まないことの証明が得られます。

しかし、形式的検証は容易ではありません。証明は元のコードの何倍もの大きさになることがあり、それを作成するには多大な労力とニッチで高度に専門化されたスキルセットが必要です。例えば、seL4オペレーティングシステムカーネルの実装には2人年かかりましたが、それを形式的に検証するには20人年かかりましたto formally verify it。したがって、形式的検証は、Airbusの航空電子機器コードのような、真にミッションクリティカルなアプリケーションにのみ実用的でした。

しかし、LLMはそれをはるかに容易にしています。最先端のモデルは、現在、現実世界のソフトウェアの正当性証明を完全に自律的に生成できます。これを実証するために、Claudeに123のオープンソースライブラリ全体にわたって有用なセキュリティプロパティを証明するように依頼しました。これには、それらの実行可能成果物の一部が特定の条件下で決してクラッシュしないことを示すことも含まれます。具体的には、Claudeは、これらのプログラムが、64MB未満のすべての入力、およびモデル化されたLinuxオペレーティングシステム（OS）の応答とメモリレイアウトに対して、常にメモリ安全性エラーやアサーション失敗を引き起こすことなく正常に終了することを証明しました。これは、すべての可能なバグを修正することからはまだ程遠いですが、以前よりもはるかに近づき、そのためのロードマップを提供します。

私たちは、これらの証明のサブセットを公開します。これにより、誰でも検証および再利用できます。また、RISC-VおよびOSセマンティクスも公開します。Theorem、このプロジェクトの協力者は、他のオープンソースプロジェクトに対しても同じパイプラインを実行することを申し出ており、開発者が独自のコードの検証を開始するのに役立つClaudeスキルを公開しています。

形式的検証は、多くの方法論を持つ広範な分野です。以下では、他の形式的検証手法を使用して、zlib圧縮アルゴリズムのセキュリティ評価、Rustで書かれたPythonインタプリタの動作等価性の証明、および重要なソフトウェアにおける長年のバグの根絶など、他のセキュリティまたはソフトウェア開発タスクを加速するための初期の調査についても説明します。

形式的検証の今後の道のりは有望です。モデルがよりインテリジェントになるにつれて、証明を作成するコストは低下しています。さらに、より多くのコードが形式化され、セキュリティ保証を達成する方法が標準化されるにつれて、コードベース間で証明を再利用または変更する能力により、コストが償却されます。以前に能力の低いモデルで試してうまくいかなかった開発者も含め、すべての開発者にLLMによる形式的検証の実験を奨励します。

この投稿の残りの部分では、形式的検証の実験について詳しく説明します。

Turning tests into proofs

ソフトウェアの一部が正しいことを証明するには、まず「正しい」とはどういう意味かを述べる必要があります。正当性は仕様（spec）によって定義されます。一部のプログラムでは、プログラムの意図された動作を形式的に仕様化する明確な方法があります。例えば、PNGデコーダーはバイトシーケンスを受け取り、（RFC 2083に従って）これらのバイトを対応する画像にデコードします。しかし、ほとんどのプログラムでは、物事はそれほど単純ではありません。テキストエディタやウェブブラウザが「正しい」とはどういう意味でしょうか？包括的で曖昧さのない仕様を取得することの難しさは、より大規模なスケールでソフトウェアを検証する上での大きな障害です。

証明しようとしたオープンソースライブラリのコードに対してこれを解決するために、既存のコンパイル可能なテストスイートを、任意のRISC-Vコンパイル済みバイナリをLinux上で実行することの意味に関する一般的なモデルを使用して、「このテストスイートは常にパスする」というルールをエンコードすることによって、仕様に自動的に変換するアプローチをとります。歴史的に、数万ものアセンブリ命令のすべての可能な動作と相互作用を包含し、それらについて議論できる証明を作成することの固有の複雑さ（および結果として証明が非常に大きくなるという事実）を考えると、そのような仕様の証明は実行不可能でした。ここで今日のLLMが登場します。明確に定義された目標を追求して何百万行ものコードを処理することは、LLMが非常に適したタスクです。

このプロジェクトでは、ファズテストから始めました。これらのテストでは、開発者はコードへのエントリポイント2を記述し、入力を受け取ります。クラッシュを引き起こすような入力は、作成者が気にするバグとなります。次に、ファザー（テストエンジン）が、バグを見つけるためにエントリポイントに膨大な数の半ランダムおよび変異した入力を生成します（図1参照）。ファザーが実行時間が長いほど、より多くのバグを見つけることができます。しかし、これは本質的に総当たりプロセスであり、試行する入力の数に関係なく、すべての可能なコードパスを実行することが保証されていません。

［動画: Fuzzing works by running huge numbers of generated inputs through one entry point to find the inputs that cause a crash. There are infinite inputs, so the search can never be complete.］

ファズテストによって表面化されたすべてのバグを見つけるために、ファズテストをコンパイルされたRISC-V命令に対する仕様に変換しました。仕様は、ファズテストが64MB未満の任意の入力に対してクラッシュしないことを示します。3 Claudeがこの仕様を証明できれば、RISC-V上のファジングは不要になります。そのエントリポイントをファジングしても、バグは見つからなくなります。

GoogleのOSS-Fuzzイニシアチブの数百のプロジェクトに対してこれを行いました。OSS-Fuzzは、適格なオープンソースプロジェクトに対して継続的なファズテストを提供します。OSS-Fuzzには、クラッシュさせること（例えば、アサーション失敗時）によって壊れたコードプロパティを探す、開発者が作成した数千のエントリポイントが含まれています。OSS-Fuzzは、CおよびC++プログラムにAddressSanitizer4（ASan）を自動的にインストラメントし、メモリが不適切にアクセスされたときにクラッシュするようにします（これはソフトウェア脆弱性の主な原因です）。メモリ安全性のような広範な仕様は、ほぼすべてのソフトウェアに適用されます。

［動画: The open-source library and its existing fuzz test are compiled to a RISC-V executable. This executable, along with Theorem’s RISC-V and OS formal semantics and the desired no-crash property, mechanically yield a specification the proof must satisfy. Claude writes the proof; the Rocq kernel checks it against the specification. Green marks what’s proven, conditional on the trusted components being correct.］

数週間にわたり、Claudeは発見したバグを修正し、123の異なるOSS-Fuzzライブラリにわたる239のエントリポイントで、任意の入力（64MBまで）に対してクラッシュがないことを証明することに成功しました。 これらの証明は、コンパイルされたRISC-V命令（つまり、実行可能バイナリ）に対して実行され、約1億8000万行のRocqで構成されています。典型的な証明は、約60万行に達し、中央値で18,000のRISC-V命令を持つバイナリにセキュリティ保証を提供します。これらの証明は、TheoremのRISC-V命令およびLinuxプロセスセマンティクスを使用して、RISC-Vアセンブリコードを数学的モデルに変換することによって構築されます。これは、これらの証明が現在、プログラムがLinux OSを使用するRISC-V CPU上で、単一スレッドの静的バイナリとして、固定メモリ予算で実行されることを前提としていることを意味します。これらの証明の範囲を拡大することは十分に可能です。なぜなら、より多くのアセンブリアーキテクチャや他のオペレーティングシステムプロセスに対するセマンティクスを標準化することになるからです。Claudeが書いた証明に関する専門家の見解を参照してください。

［動画: A formal no-crash proof over all inputs rules out all crashes along any path reachable from the entry point. While iterating on its proof, Claude can also find and fix any remaining reachable crash-producing bug.］

これは膨大な量の証明コードですが、そのほとんどは手動レビューを必要としません。Rocq証明チェッカーは、仕様が証明によって正しく満たされていることを保証します。その結果、開発者が信頼する必要がある成果物は次のとおりです。

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

これは、これらのライブラリにバグが全くないことを意味するわけではありません。むしろ、残りのバグは、上記の信頼された成果物内にあるか、Claudeの証明の範囲外にあることを意味します。これらのまだバグがある可能性のある信頼されたコンポーネント（Rocq、RISC-V、およびLinuxセマンティクス）を強化することは、無視できないことですが、スケーリングされた証明がカバーするコードのすべての行をデバッグするよりもはるかに管理しやすいタスクです。特に、このアプローチは、信頼されたコンポーネントのサイズを増やさずに、任意の数のプロジェクトを保護できるためです。

私たちは、私たちの証明の独立した検証を歓迎し、私たちの方法論の改善を奨励します。そのために、このプロジェクトのために作成された、すでに公開されていない信頼されたコンポーネント（上記）、パッチを必要としなかったファズテストのClaudeによる完全なRocq証明、および証明できなかった他のファズテストの仕様を公開します。

Finding and fixing bugs

上記では、多くのオープンソースライブラリの開発者が作成したテスト（ファズテスト）を、Claudeが常にパスすることを証明できる仕様に変換できることを示しました。これは、残りのバグをパッチした後に行われることもあります。このため、これらの仕様を証明しようとするプロセスで、数百ものバグが発見されました。

Claudeが数百のエントリポイントの証明を試みる過程で、多くのバグが現れました。このたびにClaudeが人間を待たなくても済むように、Claudeに発見したバグを修正させました。コードをパッチすると、そのパッチされたコードで仕様が再生成され、Claudeはその新しい仕様の証明を続行しました。6

私たちが発見したバグの多くは、ファザーが発見しにくいものです。ファザーは小さな入力を変異させ、通常1MBに制限されており、通常はコードカバレッジに依存してバグに誘導します。あるライブラリのエントリポイントを証明する際、Claudeはデコンプレッサーのコピー内でカウンターアンダーフローを発見し、それが境界外書き込みにつながりましたが、それは約20MBの入力で、まれで特定のレイアウトを持つ場合にのみ発生しました。他のバグには、64MBの入力と2GB以上のメモリを必要とした画像デコーダーでの境界外読み取り、同じファイルへの2つのハンドルに対する特定の呼び出しシーケンスを必要とした別のライブラリでの境界外読み取り、そして深くネストされた入力が必要だったlibexpatでのCVE-2026-56132の再発見が含まれます。Claudeは、クラッシュしない論理バグも発見しました。例えば、あるライブラリがメモリ安全であることを証明する際に、アプリケーションがロードできるファイルを制限する機能が常に強制されているわけではないことに気づきました。

このプロジェクトの最終目標は、RISC-Vコンパイル済みファズテストに残りのクラッシュがないことを証明することでした。しかし、上記のバグは、その目標が達成されたかどうかにかかわらず、プロセスが別の利点をもたらすことを示しています。このプロセスを試みるだけでも、修正が必要な実際のバグが発見されます。

Proving more than memory safety

ファズテストにクラッシュが残っていないことを証明することは、言うよりも重要です。現実世界のコードにおけるファズテストは、エンコード・デコードのラウンドトリップ、冪等性、代数法則、差分テスト、自己整合性、または参照実装との等価性など、意味のある高レベルのプロパティの違反をテストすることが一般的です。例えば、LZO圧縮アルゴリズムのファズテストは、入力を圧縮してから解凍すると、結果がオリジナルと同じであると主張します。プロパティが満たされない場合、プログラムはクラッシュします。したがって、テストが決してクラッシュしないことを証明することは、プロパティ自体を証明することと同等です。

これは、プロパティが開発者によって直接指定されていない場合でも発生する可能性があります。例えば、cpp-httplibのOSS-Fuzz証明を完了するために、Claudeはstd::setのデストラクタでの過度の再帰によるスタックオーバーフローの可能性を排除する必要がありました。この再帰深度はツリーの最大深度によって制限されるため、Claudeは（マシンコード上で！）libc++の赤黒木再バランシングアルゴリズムがツリーの深度を対数的に制限するように正しく最適化されていることを証明する必要がありました。

Other formal verification case studies

形式的検証は広範な分野です。上記のファズテストから証明への例は、LLMが直接マシンコードに証明を適用することによって形式的検証をより広く利用可能にする一例です。

他の方法でもLLMと形式的検証を組み合わせて成功を収めています。例えば、Claudeにzlib圧縮ファイル形式を定義する技術文書であるRFC 1950の形式仕様を作成するように依頼しました。次に、Linuxカーネルのzlib実装がその仕様を正しく実装していることを証明するようにClaudeに依頼しました。上記例と同様に、Claudeはバイナリレベルでこのプロパティを証明しましたが、RISC-Vの代わりに、Claudeが生成した（そして徹底的にテストされた）x86 ISAの形式セマンティクスを使用して、x86コンパイル済みバイナリを直接証明しました。7その後、このプロセスを他の数個の広く使用されているライブラリに対しても繰り返しました。その過程で、いくつかの軽微な（悪用不可能な）コーナーケースのバグを発見し、それらは現在アップストリームに提出中です。この演習から2つの結論を導き出します。（1）これらの非常にテストされたコードベースはすでにほぼ完全に正しいこと、および（2）現実の既存のコードベースに対してエンドツーエンドの正当性プロパティを証明することが可能であること。

別の実験では、ClaudeにRustでPythonの大規模サブセットのインタプリタを開発させ、学術論文に概説されているCPythonセマンティクスに準拠していることを（Verus、Rustの検証ツールを使用して）証明するように依頼しました。その後、CPythonの動作への準拠を経験的に測定し、170万以上のランダムに生成されたPythonプログラムを実行し、CPythonと99.95%のテストで同一の動作を発見しました。残りのテストの違いは、予想される既知のコーナーケースでした。

また、単純なセキュリティプロパティの形式的検証の試みを通じて、いくつかの広く使用され、重要なアプリケーションで問題を発見しました。そのうちの1つでは、10年以上潜在していた、以前は知られていなかった論理バグを発見しました。広く使用されているPDFリーダーの検証作業中に、1週間で通常1年間に報告されるのと同じ数のセキュリティバグを発見しました。

これらの取り組みの詳細は付録を参照してください。

This is just the beginning

LLM支援形式的検証の主な制限の1つは、証明に数億トークンかかる場合があることです。これらの手法をソフトウェアエコシステム全体で利用可能にすることが目標である場合、コスト効率が重要です。幸いなことに、効率が向上すると予想される説得力のある理由があります。

Newer models need fewer tokens

現実のOSS-Fuzzコードから36の小さな検証タスクを作成しました。Opus 5.5は、Opus 5よりも約40%少ないトークンでそれらの半数を証明します。モデルが長い検証タスクでトレーニングされるにつれて、この傾向は続くと予想されます。

［画像: Line chart of the share of 36 verification tasks completed by token budget per agent for Opus 5.5, Fable 5.1, and Opus 5. Opus 5.5 finishes proofs with the fewest tokens.］

Opus 5.5は、以前のモデルよりも少ないトークンで証明を完了します。 Opus 5.5、Fable 5.1、およびOpus 5のエージェントごとのトークン予算別に完了した36の検証タスクの割合。各タスクは、5Mトークンの予算で3回の独立したシングルエージェント試行を受け、最初の試行が完了したときに証明済みとカウントされます。

Proofs can be reused

エージェントが別々に作業すると、しばしば多くの労力を重複させます。証明は、ソフトウェアと同様に、小さな証明から再帰的に構築されます。そして、証明が小さいほど、再利用性が高くなる傾向があります。この影響を測定するために、エージェントが自分のターゲットを証明する際に、互いの証明をコピーできるようにしました。この共有ワークスペースにアクセスできた場合、エージェントは単独で作業した場合よりも17%少ないトークンで済み、一部のエージェントは単独で作業したときに失敗した後でも成功しました。

［画像: Chart of 36 proofs in finishing order, with arcs joining proofs that share a file and bars showing the tokens spent on each proof compared with an agent working alone.］

共有ワークスペースからの36の証明を、完了順に示します。 アーチはファイルを共有する証明を接続し、バーは各証明に費やされたトークンを単独で作業するエージェントと比較して示しています。黒線は、単独で作業するエージェントの同じタスクの平均コストを示しており、これは完了した34の証明のうち30で高くなりました（単独で作業するエージェントは2つの証明を完了できませんでした）。

OSS-Fuzz証明の取り組み中に、大規模でも同様の現象が観察されました。証明の大部分は、すべてのプログラムに含まれるコード（特にCランタイムとAddressSanitizerの初期化）に関するものであるため、非常に異なるプログラムでも大幅に重複する証明になることがあります。エージェントチームは、他のチームの完了した証明をコピーし、それを独自のプログラムに適合させることでこれを活用しました（図6）。

［画像: Block chart of the proofs for libcups, freerdp, and libzmq, showing how much of each part was identical, lightly edited, edited more or new.］

エージェントは既存の証明をコピーし、それを各新しいプログラムに適合させました。 各列は、プログラムごとの完全な証明をバイトの共有で表します。ブロックは証明の一部であり、各ブロックは同一に保持された部分、わずかに編集された部分（同じファイル、サイズが2%以内）、より多く編集された部分、または新しく書かれた部分を示しています。共有された部分は、ほとんど新しいコードを得ませんでした。

証明のこの再利用性は、Leanにおける形式数学の共有ライブラリであるMathlibが、700人以上の貢献者によって提出された約30万の定理に成長した方法です。OSS-Fuzzの取り組みの過程で同様の証明の本体を蓄積しました。その一部はリリースに含まれています（未パッチのバグを明らかにする可能性のある証明は公開していません）。

これらの初期の実験から卒業するにつれて、既存のソフトウェアの膨大な本体、特に最も重要な依存関係から検証するための戦略が必要です。示してきたように、これは汎用的な仕様を使用し、バイナリレベルで作業することで大規模に達成できます。これにより、コードベース全体を別の言語で書き直す必要がなくなります。

このアプローチは、パッケージレベルの粒度での証明の再利用も促進します。これは、各依存関係は一度だけ検証すればよいことを意味します。依存関係はべき乗則に従います。少数の共有ライブラリを証明するだけでも、膨大な量のソフトウェアを証明可能になります。詳細については、Nixエコシステム全体（glibc、OpenSSL、cURLなどの重要なインフラストラクチャを含む）を検証するためのTheoremのロードマップを参照してください。

Limitations

実際には、形式的検証は、コードのセキュリティについて望むほど多くを証明できない場合があります。

「形式的に検証済み」は「バグがない」を意味しません。 Claudeは、コンパイルされたプログラムの動作が形式仕様の要件を満たしていることを示す証明を作成できます（これは外部証明チェッカーによって検証されます）。しかし、証明チェッカーは、仕様が現実に合っているかどうかを教えてくれません。現実に合わせるためには、仕様は、検証されたプログラムが実行される現実世界の機械、CPUやオペレーティングシステムを含む、すべてを正しく包含しモデル化する必要があります。検証済みコードにバグが現れるのは、仕様、または機械の仮定されたセマンティクスが現実と異なるためです。幸いなことに、これは残りのバグを探すべき場所であり、それらのまだバグがある可能性のあるギャップを最小限に抑えるシステムを設計する方法も示しています。以下は、これらの証明にどのように適用されるか、およびそれらのギャップを埋める将来の作業のアイデアです。

実際の機械は、モデルが記述しないことを行います。 私たちの証明は、単一スレッドの静的RISC-Vバイナリで、musl libcにリンクされたものです。しかし、ほとんどの人はこれらのライブラリをx86またはARM上で実行し、glibcに動的にリンクします。このギャップを埋めるには、展開されたシステムにより近いシステムモデルが必要になります。例えば、これに向けた一歩は、x86の正確なセマンティクスを生成することです。

主張は、私たちが気にかけているすべてをカバーしていない可能性があります。 Google OSS-Fuzzの多くのファジングエントリポイントで、64MB未満の任意の入力に対してクラッシュが発生しないことを証明しました。これにはASanクラッシュも含まれます。しかし、ASanはすべてのメモリ安全性バグを検出するわけではなく、各ライブラリのすべてのエントリポイントを検証したわけではありません。たとえそうしたとしても、すべてのエントリポイントを検証したとしても、ライブラリ全体がカバーされるわけではありません（特にデッドコードがある場合）。さらに、実際のプログラムはライブラリを誤用し、呼び出し元でメモリ破損を引き起こす可能性があります。このギャップを埋めるには、呼び出し元が各公開関数に対して行うべきことを指定する必要があり、呼び出し元はそれに厳密に従う必要があります。

LLMを形式手法に活用する方法についてさらに学び、モデルが改善し続けるにつれて、これらの制限は管理可能になり、私たちが依存しているコードのより大きな割合を検証できるようになると予想しています。

Conclusion

軌跡は明確です。歴史的に、最も安全性が重要なコードにおける専門家が手作りしたカスタム保証にしか実用的でなかった形式的検証は、今日、ほとんどすべての本番ソフトウェアにとってファジングと同様に実用的になるでしょう。静的型付け、テストフレームワーク、その他の正当性ツールと同様に、検証はLLMだけでなく、言語設計や開発ワークフローのイノベーションによっても、「後付け」から「組み込み」へと成熟するでしょう。

LLMがますます多くのコード脆弱性を自動的にスキャンして発見する今日の世界では、コードのセキュリティプロパティを保証できるプロセスを使用する必要があります。LLMスケールの形式的検証は、これまで達成できなかった範囲と規模でこれらの保証を確保するための有望なアプローチです。堅牢なソフトウェアが広く普及し、ソフトウェアバグが十分に理解され、迅速に対処可能なまれなものとなる世界を共同で構築できるように、他の人々にも実験を奨励します。

付録全体を読む。