Anthropic の Frontier Red Team は10月22日、Theorem 社と組み、AI の Claude を使って123のオープンソース・ライブラリを形式検証したと発表した。64MB 以下のどんな入力を与えても、プログラムがメモリ破壊や異常終了を起こさずに終わることを、数学の証明として示したという。
Anthropic Frontier Red Team 発表 10月22日 (123 ライブラリ・239 の入口・前提と注意書き)anthropic.com
画像を開く、圧縮ファイルを解く、PDF を読む。日々のアプリが黙って使っている部品の安全を、テストの回数ではなく証明で確かめる道が、人の手で何年もかかる作業から AI が数週間で進める作業へ近づいた話だ。
何を、どこまで証明したのか
対象は、Google が運営する OSS-Fuzz というバグ探しの仕組みに登録されたライブラリで、入口にあたる関数239か所の証明を作った。各プロジェクトがもともと持っていたファズテスト (大量のでたらめな入力を流し込んで不具合を探すテスト) を、そのまま「満たすべき仕様」に読み替えている。
証明は Rocq という証明支援系で書かれ、総量は約1億8000万行、1件あたりの典型は約60万行になる。コンパイル後の RISC-V の機械語を直接相手にしているのが特徴で、Anthropic は、知る限り AI で実際に使われているソフトにこの水準の形式検証を大規模に当てた初めての試みだとしている。
途中で見つかったバグは数百に上り、中には何兆回ものテストをくぐり抜けて何年も見逃されていたものもあった。Claude は見つけたバグを修正し、修正後のプログラムについて改めて証明を作った。XML を読む libexpat では、深い入れ子の入力で起きる既知の脆弱性 CVE-2026-56132 を独自に見つけ直している。別の試みでは、ある PDF リーダーについて、通常1年分に相当する数のセキュリティ上のバグを1週間で見つけたという。
「証明済み」でも、守られない範囲がある
この成果は、範囲つきで読む必要がある。証明は、1本の処理だけで動き、決まったメモリ量の中で、Linux 上の RISC-V の CPU で動く、musl という C ライブラリを静的に組み込んだプログラムを前提にしている。実際に多く使われるのは x86 や ARM の CPU と、glibc を動的に読み込む形で、このずれは発表自身が認めている。
Anthropic は「形式検証済み」はバグがないことと同じではないとも書く。証明の価値は仕様と機械のモデルの正しさに左右され、証明の外側や、信頼して置いた部品の中にはバグが残りうる。すべての入口を証明したわけではなく、呼び出す側の使い方が誤っていればメモリは壊れうる。1件の証明に数億トークンを使うこともあり、費用も軽くない。
AI が証明を通すために「落ちないようにプログラムを書き換える」近道を取る危険もある。チームは修正に減点を課し、修正の中身をすべて記録して点検したという。
使う側と作る側に、何が届くのか
多くの人にとって、効き目はアプリやOSの更新という形で静かに届く。修正の済んだライブラリが新しい版として配られ、それを組み込んだアプリが更新されて、ようやく手元の端末が守られる。更新を後回しにしていれば、証明の成果は届かない。
作る側には、もっと直接の道具になる。証明の一部と、RISC-V と Linux の動作を形にした定義は GitHub で公開され、Theorem は他のオープンソース・プロジェクトにも同じ手順を走らせると申し出ている。まだ修正されていないバグが分かってしまう証明は、公開を控えている。
小さなライブラリを1人で保守している人にとって、ファズテストを書いておくことが、そのまま証明の入口になる。テストを持たないプロジェクトは、この流れに乗りにくい。
次に確かめたいのは、Theorem が GitHub で公開している theorem-labs/oss-verify-proofs のリポジトリに、修正の済んだライブラリの証明がどれだけ追加されていくかだ。
ことば
- 形式検証 — プログラムが仕様どおりに動くことを、テストのように試すのではなく、数学の証明として確かめる方法。網羅性は高いが、これまでは専門家が年単位の手間をかける必要があった。
- ファズテスト — でたらめな入力を大量に自動で流し込み、プログラムが落ちる入力を探すテスト。今回はこのテストを、証明が満たすべき仕様として使った。
- OSS-Fuzz — Google が運営し、重要なオープンソース・ソフトに継続的にファズテストをかける仕組み。多くの基盤ライブラリが登録している。
あなたの端末で、更新の通知を何日くらい寝かせたままにしているだろうか？
