Anthropic（アンスロピック）、Claude（クロード）にOSS 123ライブラリ・239エントリポイントの「クラッシュしない」を機械語レベルで証明させたと発表Theorem協力、証明の公開は一部

Anthropic（アンスロピック）は2026年10月22日（現地）、Theoremとの協力で、Claude（クロード）にオープンソースのライブラリ123個の「クラッシュしない」ことを形式的に証明させたと発表した。Anthropicの公式ページによると、対象はGoogleのOSS-Fuzzに登録された239のエントリポイントで、証明はソースコードではなくコンパイル後のRISC-V機械語に対するもの。証明の過程で、何兆回ものテスト実行をくぐり抜けて長年見つかっていなかったバグも見つけたという。証明の一部とRISC-VとLinuxプロセスの形式モデル（意味論）は公開されており、Theoremは条件を満たす他のOSSにも同じ処理を無料で行うとしている。

3行まとめ

1. Anthropicは10月22日、Claudeが123のOSSライブラリ・239エントリポイントについて「64MB未満のどの入力でもクラッシュしない」ことを機械語レベルで証明したと発表（約1.8億行のRocq）
2. 前提は「単一スレッド・静的リンクのRISC-Vバイナリ、固定メモリ予算、Linux」。「形式検証済みはバグなしの意味ではない」とAnthropic自身が限界を明記
3. Theoremは条件を満たすOSSに無料で同じ検証を提供するとしている。公開済みの証明は、TheoremのGitHubのREADMEによると25ライブラリ・60エントリポイント分

本記事の内容は、日本時間10月23日7時台に公式ページで確認したものです。

何を証明したのか

Anthropicの説明では、証明したのは次の性質だ。対象のプログラムは、64MB未満のどの入力に対しても、またモデル化されたLinuxのどの応答・メモリ配置に対しても、メモリ安全性のエラーやアサーション失敗を起こさず正常に終了する。

元になったのは、開発者がすでに書いているファズテスト（ランダムに近い入力を大量に流してクラッシュを探すテスト）だ。Anthropicは、ファズテストの「このテストは必ず通る」という規則を、コンパイル後のRISC-V命令に対する仕様に自動変換した。Claudeはこの仕様を満たす証明を書き、Rocqの証明検査器がその正しさを機械的に確かめる。同社は、この証明が通れば、RISC-V上でそのエントリポイントをファジングしてもバグは二度と見つからない、と説明している。

数字は次のとおり（いずれもAnthropic発表）。

証明の量は膨大だが、証明そのものを人が読む必要はほぼなく、開発者が信頼しなければならないのは、RISC-VとLinuxプロセスの形式モデル、証明した定理の文面、Rocq検査器の3つだとAnthropicは書いている。

どんなバグが見つかったのか

Anthropicによると、証明を試みる過程で数百件のバグが見つかった。Claudeは見つけたバグを自分でパッチし、仕様を作り直してから証明を続けた。パッチで「何もしないプログラム」にすり替える不正を避けるため、パッチにはペナルティを課し、パッチが挙動を変える入力がどれで、どれだけ少ないかを証明すれば加点した、ともある。パッチは記録して監査したという。

具体例として、公式ページは次を挙げている。

• あるライブラリが内部に持つ解凍処理のコピーで、約20MBかつ特定の配置の入力でだけ起きるカウンタのアンダーフローと範囲外書き込み
• 画像デコーダで、64MBの入力と2GB超のメモリが必要な範囲外読み取り
• 別のライブラリで、同じファイルへの2つのハンドルにまたがって特定の順に呼び出すと起きる範囲外読み取り
• libexpatのCVE-2026-56132の再発見（深くネストした入力が必要）
• クラッシュしない論理バグ。アプリが読み込めるファイルを制限する機能が、常には効いていなかった

Anthropicは、ファザーは通常1MB程度までの小さな入力を変異させるため、こうしたバグは見つけにくいと説明している。

他の検証事例

公式ページは、ファズテスト以外の試みも短く紹介している。

• LinuxカーネルのzlibをRFC 1950の仕様に照らし、x86のバイナリで証明。ほかのライブラリ約6本でも繰り返し、悪用できない軽微なバグを見つけた（上流に報告する手続き中）
• ClaudeにPythonの大きなサブセットのインタープリタをRustで作らせ、論文に記されたCPythonの意味論に従うことをVerusで証明させた。170万本超のランダムなPythonプログラムで試すと、99.95%のテストでCPythonと同じ挙動だった
• 広く使われているPDFリーダーの検証では、1週間で通常1年分に相当する数のセキュリティバグを見つけた
• 10年以上潜んでいた論理バグを見つけた事例もある

詳細は公式ページが示す付録（PDF）にあるとされているが、本記事では付録を取得していない。

誰がいつから使えるのか──無料のOSS Verifyと公開された証明

発表と同時に、Theoremは「OSS Verify」を案内している。Theoremの説明では、条件を満たすOSSプロジェクトは無料で、ファズターゲットが「どの入力でもクラッシュしない」ことの機械検査済みの証明を受け取れる。途中で見つかったバグは非公開でメンテナーに連絡される。

「見つかった問題やパッチはAIが生成し、送信前に人が確認する保証はない」とも書かれている。受け取る側のメンテナーは、この点を知っておく必要がある。

公開されている証明は、Theoremの oss-verify-proofs リポジトリで確認できる。READMEによると、25ライブラリの60エントリポイントに証明があり、Rocq 9.2.0で検査される（Theoremが書いた部分はMITライセンス。Anthropicの証明をもとにしたものはApache 2.0かMITを選べる）。含まれるライブラリには、OpenSSL、zstd、simdjson、leptonica、bzip2、cJSONなどがある。Anthropicのブログは、公開するのは「パッチが不要だったファズテストの完全な証明」などで、未修正のバグが分かってしまう証明は公開しないとしている。

前と何が違うのか

Anthropicは、従来の形式検証には長年の専門家の労力が必要だったと述べている。例として、seL4カーネルは実装に2人年、検証に20人年かかったという。今回の違いとして、同社は次の2点を挙げる。

1. 機械語を直接対象にした。 ソースを別言語に書き直さず、コンパイル後のバイナリを証明対象にする。Theoremは「バイナリが実際に動くものなので、証明中に見つかるバグは本物のバグ」という立場を取っている。
2. 仕様を新しく書かず、既存のファズテストを使った。 仕様作りの難しさを、すでにあるテストを使うことで避けた。

トークン消費については、公式ページは「証明の作成に数億トークンかかりうる」ことを限界として認めている。そのうえで、36の小さな検証タスクではOpus 5.5がOpus 5より約40%少ないトークンで半数を証明したこと、エージェントどうしが証明をコピーできる環境では単独より17%少ないトークンで済んだことを示している。

Theoremの試算──nixpkgs全体を検証すると約1.34億ドル

Theoremは別の記事（2026年9月29日公開、10月19日に追記）で、nixpkgsの機械語の95%を約1.34億ドルで検証できるとの試算を出している。ただし前提つきだ。モデルの検証能力が2か月ごとに倍になる傾向が続くこと、年1億ドルの予算で進めることを置いている。2か月ごとに倍という値は、Theorem自身が36個の小さなCプログラムで測った結果をもとにしている。これはTheoremの試算であり、Anthropicの発表ではない。

取得ページを見て気づいた数字の差

日本時間7時3分にAnthropicのページとTheoremのGitHubを続けて取得したところ、証明の数が2つあった。ブログ本文は「123ライブラリ・239エントリポイント」、GitHubのREADMEは「25ライブラリ・60エントリポイント」に証明があるとしている。ブログは公開が一部であることを明記しているので矛盾ではないが、「公開されている証明で第三者が確かめられる範囲」は前者より小さい。READMEにはOSS-Fuzz全体について、1,381プロジェクトのうち427でビルドでき、20,164件の定理文のうち138件が証明済み、19,797件が未着手、という数字もある。こちらは「ステートメント」単位の集計で、ブログの「エントリポイント」単位とは数え方が異なる。

発表から分かる限界と確認できていないこと

Anthropicは「形式検証済みはバグなしを意味しない」と明記し、限界を次のように書いている。

• 証明は単一スレッド・静的リンク・musl libcのRISC-Vバイナリが対象。多くの人が使うx86やARM、glibcの動的リンクとは異なる
• AddressSanitizerが検出しないメモリ安全性のバグは対象外。全エントリポイントを検証したわけでもなく、検証してもライブラリ全体がカバーされるわけではない
• 呼び出し側がライブラリを誤用して起こすメモリ破壊は対象外
• 信頼する部品はRocq、RISC-V、Linuxの意味論。これらに誤りがあれば証明の保証は崩れる

GitHub側のREADMEも、LPS（Linuxプロセスのモデル）は「ベストエフォートで不完全」で、検査対象のバイナリはclang 20.1.8でmuslに対して作ったものだと明記している。さらに、READMEによれば「止まらない実行」は除外されておらず、今回の公開リリースにはその点を証明したものはない。

本記事は、証明を自分で検査していない。Rocqでの検査も、OSS Verifyへの申し込みも試していない。数字と主張はすべてAnthropicとTheoremが公開したページによるもので、Anthropicは「専門家による証明の評価」（付録と同じPDF）を案内しているが、本記事ではそのPDFを取得しておらず、中身は確かめていない（Anthropicは独立した検証を歓迎するとしている）。日本の読者向けの提供条件や日本語の案内は、今回取得した4ページには書かれていない。

出典と確認時刻

• Formally verifying real-world software with Claude — Anthropic（2026年10月22日公開、日本時間10月23日7時3分に取得）
• OSS Verify — Theorem（日本時間10月23日7時3分に取得）
• theorem-labs/oss-verify-proofs — GitHub（日本時間10月23日7時3分に取得）
• Bootstrapping the Verified Software Stack — Theorem（日本時間10月23日7時3分に取得）

Anthropicのブログが示す付録PDFは今回取得していません。本記事は続報があり次第更新します。