Claudeが123のオープンソースライブラリの安全性を数学的に証明、1億8000万行の証明をAIが生成

AnthropicとTheoremは2026年10月22日、AIモデル「Claude」を使い、123のオープンソースライブラリに含まれる239のテスト入口について、一定の条件下でクラッシュしないことを数学的に証明したと発表した。テスト入口とは、さまざまな入力を受け取ってライブラリの機能を呼び出す、テスト用のプログラムを指す。従来のファジングが大量の入力を実際に与えて不具合を探すのに対し、今回の研究では、実際に試していない入力も含め、定められた条件を満たすすべての入力についてエラーが発生しないことを証明する。ただし、証明は特定の実行ファイルと実行環境を前提としており、公開された証明には、プログラムが必ず実行を終了することまで保証するものは含まれていない。

今回の成果が注目されるのは、専門家による多大な作業を必要としてきた形式検証を、AIによって既存のソフトウェアへ大規模に適用した点だ。一方で、証明が成立する条件は厳密に定められており、ライブラリ全体の安全性や、一般的なPC・サーバー環境での動作まで保証するものではない。どこまで証明できたのか、その保証がどの条件で成立するのかを正確に理解することが、この研究を評価するうえで重要になる。

既存のファジングテストを「すべての入力に対する証明」へ

今回の研究では、人間がソフトウェアの仕様を一から形式的に記述する代わりに、GoogleのOSS-Fuzz向けに開発者が用意していた既存のテストを活用した。ファジングは、ランダムに生成した入力や既存の入力を変化させたものをプログラムに与え、クラッシュなどの不具合を探すテスト手法だ。実行回数を増やせば多くの不具合を発見できる可能性があるものの、考えられるすべての入力を試すことはできない。一方、形式検証では、プログラムが満たすべき性質を数学的に記述し、その性質が対象範囲のすべての入力について成立することを証明する。今回の研究は、既存のファジングテストが失敗しないという条件を形式仕様に変換し、実際には試していない入力についても同じ性質が成立することを示そうとするものだ。

Anthropicの研究発表によると、研究チームは数週間で、123のオープンソースライブラリに含まれる239のテスト入口について、バグの修正を経たうえで証明を完成させた。作成されたRocq形式の証明は合計約1億8000万行に達し、対象となったのはRISC-V向けにコンパイルされた実行ファイルである。Claudeが証明を作成し、その証明が定められた性質を数学的に導いているかどうかを、Rocqのカーネルが機械的に検査する。つまり、AI自身の「正しい」という判断をそのまま受け入れるのではなく、独立した証明検査器によって正しさを確かめる仕組みだ。これまで専門家の作業負担が大きな障壁となっていた形式検証を、既存のソフトウェアへ大規模に適用したことが今回の成果である。

既存のテストを仕様として利用する場合、何を証明できるかは、そのテストが何を確認しているかによって変わる。例えば、圧縮ライブラリのLZOには、データを圧縮してから展開すると元のデータに戻ることを確認するテストがある。このテストでは、圧縮・展開後のデータが元の入力と一致しなければ失敗するため、テストが失敗しないことを証明できれば、単にメモリの不正アクセスが起きないだけでなく、圧縮と展開の結果が一致するという機能上の性質まで保証できる。ただし、証明できるのはあくまでテストに組み込まれた条件であり、テストに記述されていない要求までAIが自動的に発見し、ソフトウェア全体の正しさを保証したわけではない。

公開された証明が保証する範囲と、その限界

Theoremが公開したGitHubリポジトリには、25のライブラリに含まれる60のテスト入口について、機械的に検査可能な証明が収められている。これは、研究全体で達成したとされる123ライブラリ・239入口の一部に当たる。Anthropicは、公開対象をバグ修正が必要なかったテストの証明に限定しており、研究全体の成果がすべて公開されているわけではない。そのため、公表された研究成果の規模と、第三者が公開リポジトリを通じて検証できる範囲は区別する必要がある。

証明の内容を理解するうえで重要なのが、AddressSanitizer（ASan）を組み込んだ実行ファイルと、通常の実行ファイルの違いだ。ASanは、メモリへの不正アクセスなどを検出するため、プログラムに検査用コードを追加する仕組みである。しかし、検査用コードを追加したプログラムがエラーを起こさないことを証明しても、それだけで通常版も同じように動作すると保証できるわけではない。そこで研究チームは、検査用コードを組み込んだ版と通常版の双方についてエラーが発生しないことに加え、外部から観測できる動作が一致することも証明の対象とした。公開リポジトリには、ASanだけでなく、未定義動作を検出するUndefinedBehaviorSanitizer（UBSan）を対象とした証明も含まれている。

Anthropicの技術付録（PDF）の1〜2ページでは、64MiB未満の入力と、想定するメモリ配置について、通常版とASan版がエラーを起こさず、観測可能な動作も一致するという性質を定義している。一方、公開リポジトリの個々の定理には、通常版の実行が所定のメモリ予算内に収まることなど、別途明示された前提条件がある。そのため、技術付録に記載された64MiBという入力上限を、公開されたすべての定理に一律に適用できるわけではない。証明が成立する条件を判断するには、それぞれの定理文を確認する必要がある。

ここでいう「観測可能な動作」とは、標準入出力などを通じたデータの読み書き、プログラムの終了状態、最終的なファイルシステムの状態などを指す。検査用コードを加えた版と通常版が、こうした外部から確認できる結果について一致することを示すものであり、処理速度や消費メモリが同じであることまで保証するものではない。また、動作の同等性を証明しただけでは、プログラムが必ず終了することも保証できない。無限ループに入った場合と、処理を正常に終了した場合とでは、証明すべき性質が異なるためだ。

Theoremは、公開リポジトリの説明で、今回の公開版には実行の終了を保証する証明が含まれておらず、終了しない実行の可能性を排除していないと明記している。これは実際に無限ループが発見されたという意味ではなく、すべての実行が必ず終了することまでは証明していないという意味だ。したがって、今回の成果を「どのような入力でも正常終了することが保証された」と理解するのは正確ではない。

区分	証明の内容と確認すべき条件
成果の範囲	研究全体では123ライブラリ・239入口。公開版は25ライブラリ・60入口
対象となる実行環境	単一スレッド、静的リンク、muslを使用したLinux向けRISC-V実行ファイル
定理の前提条件	入力に関する制限やメモリ使用量の上限など。OSによるシステムコールの失敗をどこまで許容するかも定理によって異なる
証明される性質	定められた条件下でのエラー不在と、通常版・検査用コード付き版の観測可能な動作の同等性
保証されない範囲	公開版における全実行の終了、未検証の入口やテストから到達しないコードの正しさ、呼び出し側の誤用を含む安全性

今回の証明は、特定のRISC-V実行ファイルを対象としているため、同じライブラリであっても、x86やARM向けにコンパイルしたものにそのまま適用できるわけではない。glibcを使用する構成や動的リンクを採用したプログラムについても、同じ保証が成立するとは限らない。また、ASanやUBSanが検出できない種類の不具合は、それらの検査機能に基づく証明だけでは排除できない。ライブラリの一部のテスト入口について安全性を証明しても、その入口から実行されないコードや、ライブラリを呼び出すアプリケーション側の誤用まで検証したことにはならない。

さらに、証明が機械的な検査に合格したとしても、検証の基盤となるすべての要素が無条件に正しいと保証されるわけではない。今回の証明は、RISC-Vの命令やLinuxプロセスの動作を数学的に記述した形式モデルに依存している。このモデルが実際のシステムの振る舞いを適切に表していることに加え、証明対象となる定理文やRocqのカーネル、実行ファイルをモデルへ取り込むためのツールなども信頼する必要がある。AIが膨大な証明を自動生成できるようになっても、何を検証対象とし、どの前提で正しさを証明するかという判断の重要性は変わらない。

約20MBの特殊な入力で発覚したメモリ破壊バグ

今回の研究では、証明の作成過程で数百件のバグが発見されたことも重要な成果となっている。Anthropicによると、Claudeは証明を試みるなかで既存の実装に問題を見つけると、そのコードを修正し、修正後のプログラムに対する証明を再び作成した。最終的な証明の完成だけでなく、証明を成立させようとする過程そのものが、従来のテストでは見逃されていた不具合の発見につながったという。

特に興味深い事例が、あるデコンプレッサーで見つかったバグだ。この不具合は、約20MBという比較的大きな入力データが特定の配置になった場合に、カウンターの値が下限を下回るアンダーフローを起こし、メモリ領域外への書き込みにつながるものだった。一般的なファジングでは、比較的小さな入力を繰り返し変化させながらテストすることが多く、OSS-Fuzzでも入力サイズが通常1MB程度に制限される場合がある。そのため、約20MBのデータと特殊な配置の組み合わせが必要な今回のような不具合は、従来のファジングでは発見しにくかったと考えられる。

ファジングで不具合を発見するには、問題を引き起こす入力を実際に生成し、プログラムへ与える必要がある。一方、形式検証では、定められた性質があらゆる対象入力について成立することを示そうとするため、通常のテストでは到達しにくい条件も検討の対象になる。今回の事例では、単に20MB程度のデータを入力すれば不具合が起きるわけではなく、データの配置まで含めた特定の条件が必要だった。こうした複雑な条件を伴う不具合を見つけられることは、形式検証を既存のテストと組み合わせる利点の一つといえる。

Anthropicはこのほかにも、libexpatで深く入れ子になった入力によって発生する既知の脆弱性「CVE-2026-56132」を再発見したと報告している。発見された数百件のバグがすべて未知の脆弱性だったわけではなく、既知の問題も含まれている。また、あるライブラリでは、読み込みを許可するファイルを制限する機能が一部の条件で正しく適用されないという、クラッシュを伴わない論理的な不具合も見つかった。これは、証明に取り組む過程で、当初の検証対象だったメモリ安全性以外の問題が明らかになる場合もあることを示している。

もっとも、こうした成果は、形式検証によってすべての論理バグを発見できることを意味しない。証明が扱うのは、あらかじめ定義された性質と、その前提条件の範囲内に限られる。今回の研究が示したのは、既存のテストでは見逃されやすい不具合を、数学的な証明を作成する過程で発見できる可能性と、修正後のプログラムについて一定の安全性を保証できるという点だ。

1億8000万行の証明を、より複雑なソフトウェアへ広げられるか

今回の研究で作成された約1億8000万行の証明は、その規模自体も注目に値する。ただし、これはClaudeが人間のように1行ずつ記述した証明だけを集計した数字ではない。Anthropicの技術付録によると、成功した証明の半分以上は、Claudeが自ら作成したツールによって生成されたデータであり、命令の符号化情報やルックアップテーブルなどが含まれている。残る部分にもスクリプトによる生成内容が含まれ、成功しなかった試行まで合わせると、生成されたRocqコードは約10億行に達したという。したがって、証明の行数をそのまま人間の作業量や、検証対象プログラムの複雑さと比較することはできない。

証明の長さと、対象コードの規模が比例しない点も特徴的だ。技術付録によると、cJSONの391行のパーサー用テスト入口に対しては約63万行の証明が作成され、一方、約5万1000行のコードを含むfftw3では約48万行の証明が作成された。証明では対象ライブラリの処理だけでなく、プログラムの起動処理やC標準ライブラリのメモリ管理、ASanのランタイム、ファジング用のドライバーなども扱う必要がある。そのため、ライブラリ本体のコードが短くても、証明が膨大になる場合がある。

人間の形式検証の専門家であれば、共通する処理を抽象化し、同じ推論を繰り返さずに済むよう証明を構成することが多い。しかし、今回Claudeが作成した証明には、CPUレジスタの内容やメモリアドレスの関係、各分岐での動作などを細かく記述する傾向が見られた。研究チームによると、証明の検査だけでも1本につき30分から数CPU時間を要するという。現在のように冗長な証明を大量に生成する方法が、さらに大規模で複雑なプログラムにも通用するかは、今後の重要な課題となる。

その解決策の一つが、共通部品に関する証明の再利用だ。今回の証明には、プログラムの初期化処理やASanのランタイムなど、多くの対象で共通する部分が含まれている。こうした処理の正しさを一度証明し、別のプログラムでも利用できれば、対象ごとに同じ証明を作り直す必要がなくなる。証明の規模と検査に必要な計算資源を抑えながら、検証対象を広げられる可能性がある。

Theoremは、この方向性を「Bootstrapping the Verified Software Stack」でも示している。同社が構想しているのは、Nixのパッケージ管理システムが持つ依存関係を利用し、基盤となる共有ライブラリから順に形式検証を進め、その成果を依存先のソフトウェアでも再利用する方法だ。共通する部品の証明を積み上げることで、最終的には複雑なソフトウェア全体の検証につなげることを目指している。ただし、これは今後の開発構想であり、現時点でNixのソフトウェア群全体について検証が完了したわけではない。

第三者が成果を検証するための環境も整備されている。公開リポジトリには、公式のRocq 9.2.0を使用して証明を検査する手順が用意されており、対象となる実行ファイルの構成や、証明が成立する条件も確認できる。ただし、今回の成果はAnthropicとTheoremによる研究発表と公開資料に基づくものであり、独立した第三者によってすべての証明が再検証された結果ではない。実際の開発に応用する際には、単に使用するライブラリが検証対象に含まれているかだけでなく、どのバージョンの実行ファイルが対象なのか、どのテスト入口を通じた動作が保証されるのか、どのような前提条件が必要なのかを確認することが欠かせない。

今回の成果は、AIによる形式検証が、研究用の小規模なプログラムだけでなく、実際に使われているオープンソースソフトウェアにも適用できる可能性を示した。一方で、その保証は特定の実行ファイルや形式モデル、定理の前提条件に依存しており、ソフトウェア全体の安全性を無条件に保証するものではない。今後、共通部品の証明を再利用し、実際に利用されるビルドや実行環境へ検証対象を広げられれば、形式検証を日常的なソフトウェア開発に組み込む道が開けるだろう。