LLMで形式検証が現実的になった：Claudeが123のOSSライブラリで落ちないことを証明した

by yasuna

8 min read

Anthropic Claude 形式検証 セキュリティ テスト

この記事はAIエージェントと一緒に執筆しています

はじめに

Anthropic の Frontier Red Team が「LLMs are making formal software verification feasible at a much larger scale」という記事を出しました（2026-10-22）。Theorem という会社との共同の取り組みです。

この記事の読み方

この記事は、元の記事を Claude（AI）といっしょに読んでまとめたものです。どこまでが事実で、どこからが感想かが分かるように分けています。

  1. 元の記事に書いてあること：元の記事の内容を日本語でまとめたもの。感想は入れていません
  2. 思ったこと：作者（yasuna）のひとことと、AI（Claude）が書いた感想を分けて書いています

1. 元の記事に書いてあること

ここは、すべて元の記事（2026-10-22）の内容です。

ひとことで言うと

  • ほとんどのソフトにはバグがあって、それを AI が簡単に見つけて悪用できるようになってきた。ふつうの防御ではもう足りず、コードにバグがないことを証明する方法が要る
  • 形式検証ならそれができるが、これまでは専門家が何年もかけないとできず、ほとんどの実際のプロジェクトでは現実的ではなかった
  • Claude を使って、100を超える実際のオープンソースのライブラリについて、アセンブリ（RISC-V）のレベルでセキュリティの性質を証明した。AI で本番のソフトにアセンブリのレベルで形式検証をかけた大規模な取り組みとしては、知る限り初めて
  • 証明を書いている途中で、何兆回ものテストをすり抜けて何年も見つかっていなかったバグも見つかった
  • モデルが賢くなるにつれて、形式検証は安全なソフト開発に欠かせないものになると見ている

これまでの形式検証が大変だった理由

  • 形式検証は、コードを数式のモデルにして、決めたルールを必ず守ることを証明するやり方。証明できなければ、ルールを破るバグがあるかもしれないし、失敗の仕方からバグの見当もつく。これをくり返すと、そのルールを破るバグがないことの証明にたどりつく
  • でも、証明は元のコードの何倍も大きくなりがちで、特殊な技術が要る
  • たとえば OS カーネルの seL4 は、作るのに2人年、形式検証に20人年かかった
  • なので、これまでは Airbus の航空機のソフトのような、本当に失敗できないところでしか現実的ではなかった
  • ちなみに、とてもよくテストされている Linux カーネルでも、最近1,000件を超える脆弱性が公開された

やり方：テストを証明に変える

一番の壁は、「正しい」とは何かを決める仕様です。PNG のデコーダーなら RFC 2083 があるけれど、テキストエディタやブラウザの「正しい」を書き切るのは難しい。

そこで、ライブラリにもともとある、コンパイルできるテストを、そのまま仕様にしたそうです。「このテストは必ず通る」という形です。

  • 使ったのは ファズテスト。開発者が入り口を書いて、そこに入れたらクラッシュする入力があれば、それはバグ、というテスト
  • ふつうのファザーは、大量の半分ランダムな入力を試すので、どれだけ回しても全部の道を通った保証はない
  • これを「64MB 未満のどんな入力でもクラッシュしない」という、RISC-V にコンパイルした命令の上での仕様に変えた。これが証明できれば、その入り口をファズしても、もうバグは出てこない
  • 対象は Google の OSS-Fuzz のプロジェクト。C/C++ のプログラムは AddressSanitizer（ASan）つきでコンパイルされていて、メモリの使い方がおかしいとクラッシュする

結果

  • 数週間で、123の OSS-Fuzz ライブラリ、239の入り口について、見つけたバグを直したうえで「64MB までのどんな入力でもクラッシュしない」ことを証明した
  • 証明は Rocq で書かれていて、全部で約1億8,000万行。ふつうの証明は約60万行で、対象のバイナリは中央値で1万8,000命令
  • 前提は「RISC-V の CPU 上の Linux で、シングルスレッドの静的バイナリとして、決まったメモリの量で動く」こと
  • 証明はとても大きいけれど、人が読む必要はほとんどない。証明が仕様を満たしているかは Rocq のチェッカーが確かめる。信じる必要があるのは次の3つだけ
    • RISC-V と Linux のプロセスの形式的なモデル
    • 証明した定理の文そのもの
    • Rocq の証明チェッカー
  • 「バグがゼロ」という意味ではなく、残っているバグは上の3つの中か、証明の範囲の外にある、という意味
  • 証明の一部、RISC-V と OS の意味論を公開。Theorem は、ほかの OSS にも同じ流れを回す申し出と、自分のコードの検証を始めるための Claude のスキルを公開している

見つかったバグ

証明しようとする途中で、何百ものバグが見つかったそうです。人が毎回止めなくていいように、Claude がバグを直して、直したコードで仕様を作り直して、また証明に戻る、という流れにしていました。

ファザーではまず見つからなさそうなものが多かったとのこと。

  • 解凍の処理でカウンターがマイナスに回り込んで範囲外に書き込む。約20MB の入力で、めずらしい並びのときだけ起きる
  • 画像デコーダーの範囲外読み込み。64MB の入力と2GB を超えるメモリが要る
  • 同じファイルへの2つのハンドルで、特定の順番で呼んだときだけ起きる範囲外読み込み
  • libexpat の CVE-2026-56132 の再発見（深い入れ子の入力で起きる）
  • クラッシュしない論理のバグも。読み込めるファイルを制限する機能が、いつも効いているわけではなかった

メモリ安全より先のことも証明できる

  • ファズテストの多くは、「圧縮して解凍したら元に戻る」のような大事な性質を確かめていて、成り立たなければクラッシュするように書かれている。なので「クラッシュしない」を証明すると、その性質そのものを証明したことになる（例：LZO の圧縮）
  • 開発者が書いていない性質が要ることもある。cpp-httplib の証明では、std::set のデストラクタで再帰が深くなりすぎないことを示すために、libc++ の赤黒木のバランスがちゃんと対数の深さに保たれることを、機械語の上で証明した

ほかの形式検証の例

  • zlib の形式を決めた RFC 1950 の仕様を Claude に書かせて、Linux カーネルの zlib の実装がそれを守っていることを、x86 のバイナリの上で証明した。ほかの広く使われているライブラリでも同じことをして、悪用できない小さなバグがいくつか見つかった。結論は「よくテストされたコードはほぼ正しい」「実際のコードで端から端まで正しさを証明できる」
  • Rust で書いた Python のインタプリタ（大きなサブセット）が CPython の意味どおりに動くことを、Verus で証明。ランダムに作った170万以上の Python プログラムで試して、99.95% が CPython と同じ動きだった
  • 広く使われている PDF リーダーの検証では、ふだん1年で報告されるのと同じ数のセキュリティのバグを、1週間で見つけた。10年以上眠っていた論理のバグも見つかった

これから：コストは下がっていく

  • 弱点は、証明に何億トークンもかかること
  • 実際の OSS-Fuzz のコードから作った36の小さな検証タスクで、Opus 5.5 は Opus 5 より約40%少ないトークンで半分を証明できた
  • 証明はソフトと同じで、小さな証明を組み合わせて作るので、使い回せる。エージェント同士がお互いの証明をコピーできる場にしたら、ひとりでやるより17%少ないトークンで済み、ひとりでは失敗したものが成功することもあった
  • OSS-Fuzz の作業でも、証明の大部分は C ランタイムや ASan の初期化のように、どのプログラムにもある部分なので、別のチームの証明をコピーして手直しする形で進んだ
  • Lean の数学ライブラリ Mathlib が、700人以上の貢献で30万近い定理に育ったのと同じ形
  • 前に弱いモデルで試してうまくいかなかった人も含めて、LLM での形式検証を試してほしい、と呼びかけている

2. 思ったこと

yasuna（作者）のひとこと

記事にしてみて、面白かった。形式検証はどのソフトウェアにも必要になってくると私も思う。実コードよりテストコードが大事。

わたし（AI）が思ったこと

ここは、AI（Claude）が書いた感想と補足です。

  • 作者の「実コードよりテストコードが大事」は、この記事の作り方そのものだと思いました。今回の証明の仕様は、開発者がもともと書いていたファズテストです。テストが「このライブラリが守るべきこと」を書いていたからこそ、それを証明に変えられた。テストが薄ければ、証明できるのも薄いことだけになります
  • 証明が1億8,000万行あっても人が読まなくていい、信じるのは「モデル・定理・チェッカー」の3つだけ、という整理が分かりやすかったです。人が見るべきなのは、何を証明したか（仕様）のほうになる、ということだと読みました
  • 前の記事で読んだ OpenAI の Patch the Planet でも、「最初から脆弱性を作らない」方法のひとつに形式検証が挙がっていました。見つけて直す話と、ないことを証明する話が、同じ時期に出てきたのは面白いと思いました

まとめ

  • 【元の記事】Claude で 123の OSS ライブラリ・239の入り口について、RISC-V のバイナリが「64MB 未満のどんな入力でもクラッシュしない」ことを証明した（Rocq で約1億8,000万行）
  • 【元の記事】仕様は、もともとあったファズテストをそのまま使った。証明の途中で、ファザーでは見つからない何百ものバグが見つかった
  • 【元の記事】証明を使い回すとトークンが減り、新しいモデルほど少ないトークンで証明できる
  • 【yasuna】形式検証はどのソフトにも必要になってくる。実コードよりテストコードが大事
  • 【わたし（AI）の考え】テストが「守るべきこと」を書いていたから証明に変えられた。人が見るべきなのは、証明そのものより仕様のほう