オープンソース123ライブラリのテスト用入口239か所で「クラッシュしない」ことをClaudeが証明｜Anthropicの形式検証の仕組みと、証明が成り立つ条件

2026年10月25日

Anthropicは10月22日、Claudeで123のライブラリを形式検証したと公表した

AIのClaudeを開発するAnthropicは2026年10月22日、Claudeに数学的な証明を書かせて、オープンソースのライブラリ123件で、テスト用に用意された239か所の入口（エントリポイント）が「一定の条件のもとでは、どんな入力を与えてもクラッシュしない」ことを確かめた研究を公表しました。AIの安全性やセキュリティを調べる社内チーム（Frontier Red Team）と、検証技術の企業Theoremの共同研究です。

このように、プログラムが、あらかじめ決めた性質を必ず満たすことを数学的に証明する方法を「形式検証」と呼びます。テストは試した入力についてしか確かめられませんが、形式検証は条件に当てはまるすべての入力をまとめて扱えます。そのかわり証明を書く手間が大きく、OSの中核部分（seL4というカーネル）では、カーネルを作るのにかかったのべ2人年に対し、その検証にはのべ20人年がかかったとAnthropicは紹介しています。

今回の研究では、その証明を書く作業をClaudeが受け持ちました。この記事では、何がどの条件で証明されたのか、証明の途中で見つかったバグ、そして「形式検証済み」と書かれたソフトウェアを見るときに確かめたい前提を整理します。

研究の要点

Claudeが証明を書き、別のソフトがその証明を機械的に確かめた

証明した範囲

123ライブラリ・239か所

Googleの継続テスト（OSS-Fuzz）に参加しているライブラリで、ファズテストの入口（エントリポイント）239か所。

証明した性質

64MB未満の全入力でクラッシュしない

メモリの不正な読み書きや、テスト内の確認（assert）の失敗でプログラムが止まらないこと。

見つかったもの

ファズテストでは届きにくいバグ

20MB前後の入力でだけ起きる範囲外書き込みなど。Claudeが修正してから証明した。

公開された証明

25ライブラリ・60か所

修正なしで証明できた入口の証明を、誰でも検査し直せる形でGitHubに公開。ライブラリの開発元でまだ修正が公開されていないバグの場所を示しうる証明は、公開を控えている。

出典: Anthropic「LLMs are making formal software verification feasible at a much larger scale」（2026年10月22日）、theorem-labs/oss-verify-proofs のREADME（2026年10月24日確認）

ファズテストの「クラッシュしない」を、64MB未満の全入力で成り立つ約束にした

証明を書くには、まず「正しい」とは何かを決める必要があります。画像の形式のように仕様書がある処理は別として、多くのソフトウェアには、正しさを一つの文章で言い切れる仕様がありません。Anthropicはこの問題を、ライブラリにすでにあるテストを流用することで避けました。

使ったのはファズテストです。ファズテストは、プログラムに用意したテスト用の入口（エントリポイント）へ、自動で作った大量の入力を次々に入れ、クラッシュする入力を探す方法です。OSS-Fuzzでは、メモリの範囲外を読み書きした瞬間にプログラムを止める仕組み（AddressSanitizer）を組み込んで動かすため、メモリの扱いの誤りもクラッシュとして見つかります。

ファズテストの「どの入力でもクラッシュしない」という期待を、そのまま証明すべき約束（仕様）にしたのが今回の工夫です。約束は、ライブラリとテストを一緒にコンパイルしたプログラムの機械語を対象にします。ソースコードではなく、実際に動く命令の列そのものを対象にしています。

1. 1. 機械語にする

   ライブラリとファズテストを、CPUの設計の一つであるRISC-V向けの実行ファイルにコンパイルする。

2. 2. 約束を自動で作る

   Theoremが作った「RISC-Vの命令とLinuxのプロセスの数学的なモデル」と組み合わせ、「この実行ファイルはクラッシュしない」という証明の目標を機械的に作る。

3. 3. Claudeが証明を書く

   証明は、証明を機械で確かめるソフト「Rocq」（旧名Coq）の言語で書く。典型的な証明で約60万行、全体で約1億8000万行になった。

4. 4. Rocqが検査する

   証明が目標を満たしているかはRocqが確かめる。人が1億8000万行を読む必要はない。

証明の対象になった実行ファイルは、中央値で1万8000命令ほどの大きさです。数週間で、123ライブラリの239か所の入口について証明が完成しました。

この方式では、人が信頼すればよいものは3つに絞られます。RISC-VとLinuxのプロセスの数学的なモデル、証明すべき約束（「クラッシュしない」という定理）が意図どおりに書かれていること、そしてRocqの検査器そのものです（厳密には、Rocqを動かすハードウェアやOSも含みます）。証明の中身がどれだけ長くても、この3つが正しければ結論は正しいことになります。

証明の途中で、ファズテストでは届きにくいバグが見つかった

証明がうまく進まないとき、その原因がプログラムのバグであることがあります。Anthropicによると、証明できた239か所を含む数百か所の証明を試みる過程で、数百件のバグが見つかりました。Claudeはバグを見つけるたびにコードを修正し、修正後のプログラムに対して約束を作り直して証明を続けました。

Anthropicは、何兆回ものテストをくぐり抜けて何年も見つかっていなかったバグもあったと書いています。見つかったバグの多くは、小さな入力を少しずつ変えて試すファズテストではまず出会わない種類のものでした。報告に挙がっている例を並べます。

AIに「証明できる状態にせよ」と任せると、プログラムを何もしない形に書き換えて証明を通す、という抜け道もありえます。Anthropicはこれを防ぐため、Claudeの作業の採点で、修正すれば減点し、修正で振る舞いが変わる入力が少ないことを証明すれば加点することにし、修正の内容を記録して監査したと説明しています。

証明できるのは「クラッシュしない」ことだけに見えますが、ファズテストの中には、データを圧縮してから解凍すると元に戻る、といった性質をassertで確かめているものがあります。その場合、クラッシュしないことの証明は、圧縮と解凍で元に戻るという性質の証明にもなります。

証明が成り立つのは、RISC-V向けの実行ファイルなどの条件の中

ここまでの結果は強い保証ですが、保証が及ぶ範囲には前提があります。Anthropicの報告と、公開リポジトリの説明（theorem-labs/oss-verify-proofs）から、保証の範囲と前提を分けると次のようになります。

強い保証なので「バグがない」と受け取りたくなりますが、Anthropicは報告の中で、「形式検証済み」と「バグがない」を分けて考えるよう書いています。証明が確かめるのは、プログラムが約束どおりに動くことです。約束が本来期待する動作とずれていたり、CPU・OSのモデルが現実の機械とずれていたりすれば、そのずれの中にバグが残ります。逆に言えば、残ったバグを探す場所は、信頼する3つの要素と、証明の範囲の外側に絞り込めます。

ふだんスマートフォンやパソコンで動いているライブラリは、多くがx86やARM向けにビルドされたものです。今回の保証が付いているのはRISC-V向けの実行ファイルで、手元の版に同じ保証を広げるには、x86やARMのモデルを使った証明が別に必要になります。Claudeがバグを修正した入口では、その修正が取り込まれた版であることも条件になります。Anthropicは、ふだん使われる環境に近いx86などの正確なモデルを整えることを、証明の範囲を広げる次の段階として挙げています。

証明に必要なトークンは、新しいモデルで減っている

現時点の大きな制約はコストです。証明を作るのに、AIが読み書きする文章の量（トークン）が数億に達することがあるとAnthropicは書いています。そのうえで、コストが下がっていく根拠として2つの測定を示しました。

使い回しが効くのは、どのプログラムにも共通する部分（Cの実行環境やAddressSanitizerの初期化）が証明の大半を占めるからです。123ライブラリの作業でも、別のClaudeが完成させた証明を写して自分のプログラムに合わせる進め方が見られたといいます。

ファズテスト以外にも、zlibやPDFリーダーで形式検証を試した

報告には、ファズテスト以外の試みも載っています。

• 123ライブラリとは別の実験で、Linuxカーネルに入っている圧縮ライブラリzlibを検証した。まずClaudeがRFC 1950（zlibの形式を定めた文書）をもとに形式仕様を書き、この実験用にx86のモデルも作って大量のテストで確かめた。そのモデルを使って、x86の実行ファイルが仕様どおりに動くことをClaudeが証明した。
• Pythonの大部分を扱う処理系をClaudeにRustで書かせ、Rust向けの検証ツールVerusで、学術論文がまとめたCPythonの動作に従うことの証明にも取り組ませた。そのうえで試すと、ランダムに作った170万本のプログラムの99.95%で、本家のCPythonと同じ結果を返した。
• 広く使われるPDFリーダーを形式検証しようとする作業の中で、1週間に、ふだん1年間に報告されるのと同じ数のセキュリティバグが見つかった。

公開された証明と、自分のプロジェクトを登録する方法

今回の証明の一部は、誰でも検査し直せる形で公開されています。ライブラリを使う側とメンテナーの側で、確かめられることを順に挙げます。

1. 1. 使っているライブラリが一覧にあるか見る

   oss-verify-proofsのREADMEに、証明済みの25ライブラリ・60か所の入口が並んでいる。OpenSSL、zstd、bzip2、simdjson、libpcapなどが含まれる。

2. 2. 証明の検査結果を見る

   公開済みの全証明を検査するGitHub Actions（release-check）は、2026年10月23日の実行で成功している。自分で検査し直す場合はDockerが必要で、16コアで検査すると1件あたり最大20GiBのメモリを使う。

3. 3. メンテナーなら登録条件を確かめる

   TheoremのOSS Verifyは、中核メンテナーが登録するプロジェクトを対象に、同じ方法で証明を試みる。ファズテストが1つ以上あること、OSI承認のライセンスであることなどが条件で、見つかったバグは登録した連絡先へ非公開で届く。

OSS Verifyから届く修正案はAIが作ったもので、Theorem自身が誤りを含みうると明記しています。受け取ったら、ふだんの外部からの修正と同じように中身を読んでから取り込むのが前提です。

今回の研究で印象に残ったのは、「64MB未満のすべての入力でクラッシュしない」という強い結論を、人が読み切れない1億8000万行の証明と、人が信頼する3つの要素に分けて扱っている点です。「形式検証済み」と書かれたソフトウェアに出会ったら、どの実行環境の、どの入口について、何を証明したのかを最初に確かめると、保証の大きさを正しく測れます。