Anthropicのフロンティア・レッドチームは10月22日、Claudeを使って123のオープンソースライブラリ、計239のエントリポイントに形式証明を書かせたとする研究を公開した。入力が64MB未満であれば、これらのプログラムはクラッシュしないという内容だ。証明はコンパイル済みのRISC-V実行ファイルを直接の対象としており、形式手法ツールを手がけるTheoremと共同で進めた。Anthropicは、AIが本番ソフトウェアのアセンブリ層で大規模な形式検証を行ったのは初めてだとしている。
対象のライブラリはすべてGoogleのOSS-Fuzzプロジェクトに由来する。ファジングのプラットフォームに長く登録されてきた基盤コンポーネント群で、圧縮、画像デコード、HTTPパースなどが含まれる。作業全体には数週間を要した。
ファジングテストを定理に書き換える
手順は3段階だ。まずチームは、各ライブラリが持つ既存のファジングテスト一式を、「このテストコードは任意の入力に対してクラッシュしない」という形式仕様に書き換えた。仕様は、Theoremが提供するRISC-Vの命令セマンティクスとLinuxプロセスのセマンティクスのモデルの上に構築されている。
次にClaudeが証明を書き、Rocqの証明検査器が一行ずつ検証する。
"Claude writes the proof; the Rocq kernel checks it against the specification."
（Claudeが証明を書き、Rocqカーネルがそれを仕様と照合して検査する。）
3段階目は、証明が通らない場合の処理だ。証明が行き詰まるのは、コードに本当に欠陥があるからということが多い。その場合はClaude自身がコードを修正し、仕様を再生成して証明を続ける。チームは、この段階では「報酬ハッキング」、つまりモデルが証明を通すためだけにプログラムを無理に書き換える事態が起こりやすいと認めている。そのためパッチにはペナルティを課し、パッチが影響する入力範囲の証明を求め、すべて記録して人手で監査する仕組みにした。
典型的な証明は約60万行。最終的に信頼が必要なのは、RISC-VとLinuxのセマンティクスモデル、定理の記述そのもの、そしてRocq検査器だけになる。
証明の過程で見つかった脆弱性
証明の途中で発見・修正された不具合は数百件にのぼり、ファジングでは当てにくいものも含まれる。記事では例が挙げられている。展開（解凍）ツールのカウンタのアンダーフローは、約20MBの特定の入力でのみ発生する。画像デコーダの範囲外読み取りは、64MBの入力と2GB超のメモリがあって初めて現れる。さらに別の範囲外読み取りは、2つのハンドルが同じファイルを特定の順序で操作したときに起きる。libexpatのCVE-2026-56132も改めて見つけ出された。
cpp-httplibの証明にはさらに難所があった。std::setの破棄時の再帰がスタックオーバーフローを招くおそれがあったのだ。これを排除するため、チームはlibc++の赤黒木のバランス調整アルゴリズムが木の深さを対数オーダーに抑えることを、機械語レベルで証明した。
同じ研究には、いくつかの副次的な実験も付いている。ClaudeはRustでPythonのサブセットを書き、VerusでCPythonのセマンティクスに適合することを証明した。170万本のランダムなプログラムでCPythonと挙動が一致した割合は99.95%だった。また、x86命令のセマンティクスを自力で生成し、1ステップずつの実行でUbuntuのユーザー空間を起動できるところまで到達。その過程で公式リファレンス文書の誤りを数百件見つけ出した。
seL4と並べて見る
形式検証自体は産業界で目新しいものではなく、難しさはずっと人手にあった。業界でよく引き合いに出されるのがseL4マイクロカーネルで、Cコード約1万行に対し、当時の証明工数は20人年前後とされることが多い。CompCertコンパイラも同様の路線で、小さなチームが何年もかけて磨き上げた。こうしたプロジェクトに共通するのは、対象が少なく、期間が長く、専門家が密集していることだ。
今回のAnthropicの規模は、123ライブラリを数週間で処理するというもの。大まかに比べれば、作業単位あたりのコスト構造は別の形に変わり、人は証明を書く側から、仕様を定め、パッチを審査する側へ退いた。代わりに払うのはトークンで、記事によれば完全な証明1件に数億トークンを消費することもある。36の小規模タスクでは、1タスクにつきエージェント1つが3回試行し、1回あたり500万トークンの予算を与えた。エージェント同士が互いの証明を再利用できるようにすると、必要トークンはさらに17%減った。
保証の強さも同列ではない。seL4が証明したのは機能的正しさだが、今回証明したのは「クラッシュしない」ことだけで、範囲ははるかに狭い。
証明の外に残る空白
Anthropic自身が挙げる制約はかなり具体的だ。証明の対象は、シングルスレッドで静的リンクされ、musl libcを使うRISC-Vバイナリである。一方、多くのユーザーが実際に動かすのは、x86やARM上でglibcを動的リンクしたビルドだ。AddressSanitizer自体がすべてのメモリ安全性エラーを検出できるわけではなく、カバーされていないエントリポイントもある。呼び出し側がライブラリを誤用して起きるメモリ破壊も、証明の範囲外だ。
"Formally verified" does not mean "bug-free."
（「形式検証済み」は「バグがない」ことを意味しない。）
仕様と実機のずれは、この路線で最も問題が起きやすい部分だ。Rocqと各セマンティクスモデル自体も堅牢化が必要で、記事はこれを「小さな仕事ではない」としている。チームの見立ては、形式検証は安全なソフトウェア開発の通常工程になっていくというもの。ただし、こうした証明がx86やglibcのような主流の配備環境にいつ及ぶのかについて、記事は時期を示していない。
参考資料：Anthropicフロンティア・レッドチームの研究記事、CocoLoop、Anthropic研究ページ（ライブラリ数、エントリポイント数、証明の行数、トークン比較の算定方法を確認）。