セキュリティ

形式検証がfuzzingの隣に並ぶ日——発表の数字と、公開リポジトリの数字の差

形式検証は長らく「人的コストがボトルネック」でした。証明を書ける人が足りないので、航空・鉄道・暗号といった安全重要コードに用途が限られてきた。今回の主張は、その部分がトークン課金に置き換わったというものです。ただし発表の見出しと公開物の実体には差があります。どちらも数字で示されているので、並べて読みます。

要点

• 発表／OSS-Fuzz由来の123ライブラリ・239エントリポイントについて、「64MB未満のあらゆる入力でクラッシュしない」ことを証明したとされる
• 規模／証明の総量はRocqで約1億8,000万行。典型的な1証明が約60万行、対象バイナリはRISC-V命令で中央値18,000命令
• 副産物／作業中に数百件のバグを発見・修正。libexpatのCVE-2026-56132を再発見し、デコンプレッサのカウンタ・アンダーフローによる領域外書き込みも検出
• 公開物／ただし公開されたのは部分集合。リポジトリ側は26ライブラリ・61エントリポイント
• 全体像／全体インデックスは20,164文のうち証明済み336、反例つきで偽と判明5、モデルによるブロック229、未着手19,594
• 前提／RISC-V／musl libc／シングルスレッド静的バイナリ。x86・ARM・glibc動的リンクという実運用構成はまだ射程外

何が起きたか

Anthropicの Frontier Red Team が2026年10月22日、「LLMs are making formal software verification feasible at a much larger scale」を公開しました。Theorem Labs との共同成果です。

手法はこうです。

1. OSS-Fuzzの各fuzzターゲットとライブラリをRISC-Vにコンパイルする
2. Theorem製のRISC-V命令セマンティクスとLinuxプロセス実行モデル（LPS）を噛ませる
3. 「クラッシュしない」という性質を付けて仕様文を機械生成する（クラッシュの定義はAddressSanitizerが検出するメモリ安全性違反とアサーション失敗）
4. そこにモデルが証明を書き、Rocqのカーネルが検査する
5. バグが出ればモデル自身がパッチを当て、パッチ後のコードから仕様を再生成して証明し直す

人間が1件ごとに止まらない設計になっているのがこの取り組みの核です。

なぜ「読まなくていい証明」が意味を持つのか

約60万行の証明を人間が読むわけにはいきません。それでも成立するのは、信頼ベース（trusted base）が小さいからです。

レビュワーが信じる必要があるのは3つだけです。

1. RISC-VとLinuxプロセスの形式モデル
2. 証明された定理文そのもの
3. Rocqの証明チェッカー（およびその土台のOCamlコンパイラとOS）

証明本体はチェッカーが仕様に対して機械的に検査します。コードレビューの経済性が変わるのはここです。

再利用も効きます。各証明の多くはCランタイム初期化やASanといった共有コードを覆うため、無関係なプログラムの証明が重複する。依存ライブラリをパッケージ単位で一度検証すれば、依存する広い範囲に効きます。

エージェント側の工夫も数字が出ています。ワークスペースを共有して互いの証明をコピーさせると、36タスクのベンチでトークン消費が17%減り、共有時のみ成功するタスクもあったとされています。

公開リポジトリを読むと、話はもっと慎重になる

ここが本記事の要点です。発表の見出しと、公開リポジトリの実体には差があります。

• 発表／123ライブラリ・239エントリポイント
• 公開リポジトリ／26ライブラリ・61エントリポイント（Rocq 9.2.0で検査済み。boost-beast、cjson、openssl、simdjson、zstdなど）

さらに定理の形も、見出しの「クラッシュしない」とは違います。実際に証明されているのはサニタイザ有無の2ビルドの挙動一致です。

READMEの定義はこうです。plainビルドがメモリ予算内に収まる入力において、両ビルドともエラーに到達せず、同じ観測挙動の集合を示す。予算はASanで2GiB、UBSanで16GiB。

この形でも「サニタイザが検出しうるエラーは、その入力範囲で起こらない」ことは言えます。ただしREADME自身が範囲を明示しています。

• モデルの限界／「LPSはbest effortで完全ではない」。Linuxの一部を記述し、検査しない仮定を含む。証明はLPSの正しさを超えない
• 正しさではない／ライブラリが正しいことは言っていない。サニタイザが検出できない誤り（誤った結果、メモリリーク）は除外されない
• 範囲／ライブラリ全体ではなく、1エントリポイントが到達するコードについての主張
• 停止性／公開時点でどの証明も停止性を主張しない

全体インデックスの数字が、現在地をいちばん正確に表しています。20,164文中、証明済み336・反例つきで偽と判明5・モデルによるブロック229・未着手19,594（427プロジェクト、2,148ハーネス）。

1.8億行は「証明可能になった」ことの実証であって、OSS全体の検証が終わった話ではありません。

本記事の初出時点（2026年10月23日）では「25ライブラリ・60エントリポイント、証明済み138文、未着手19,797文」でした。2026年10月29日に公開リポジトリを再確認したところ「26ライブラリ・61エントリポイント、証明済み336文、未着手19,594文」に増えており、さらに反例つきで偽と判明した文が5件記録されていました。パイプラインは継続して回っています。

なぜ日本でまだ語られていないのか

一次ソースが発表記事、付録PDF、そしてTheorem Labsの2つのリポジトリに閉じているためです。

発表の数字と公開物の数字の差は、GitHubのREADMEまで降りないと見えません。しかもRocq（旧Coq）とfuzzingの両方を前提に読む必要がある。二次媒体が手を出しにくい構造になっています。

エンジニアにとって何が変わるか

①設計

対象はRISC-V・musl・シングルスレッド静的バイナリで、x86やARMのglibc動的リンクという実運用構成はまだ外です。明日の本番には効きません。

効くのは依存ライブラリの選定基準です。zstdやopensslのように証明が積まれるライブラリと、そうでないライブラリの差が、ライセンスやメンテ状況と並ぶ比較軸になります。Theoremは他のOSSにも同じパイプラインを回すと申し出ています。

②調達

コストはトークンに移ります。1証明に数億トークンかかるとされており、まだ自前で回す話ではありません。ただし「検証済みバイナリ」をベンダー評価の項目に入れる準備はできます。

③キャリア

価値が、証明を手書きする仕事から、仕様とモデルを書く仕事へ移ります。

報酬ハッキング対策として、パッチにペナルティを課し、パッチが変える入力の範囲を証明させ、全パッチを記録して監査したと明記されています。エージェントが「クラッシュしないようにプログラムを書き換えて定理を通す」のを防ぐ設計です。

したがってレビュワーの仕事は証明の中身ではなく、仕様文とモデルの妥当性、そしてパッチの監査になります。RocqやVerusと、脅威モデルを仕様に落とす力の組み合わせが、学術寄りだった領域から実務側に出てきます。

確認できなかった点

• 公開範囲／全239エントリポイントの証明がいつ・どこまで公開されるか
• 入力制限の対応／発表記載の「64MB未満の入力」と、リポジトリ記載のメモリ予算（ASan 2GiB／UBSan 16GiB）の厳密な対応関係
• コスト／1証明あたりの実コスト（「数億トークン」との記述のみで金額換算なし）
• x86／x86セマンティクスはzlibのケーススタディで生成されたとあるが、その成果物の公開状況
• 第三者検証／外部による証明の再検査結果。検証手順は公開されているが、追試の報告は確認できていない

出典

• 一次／Anthropic「LLMs are making formal software verification feasible at a much larger scale」（2026年10月22日）および付録PDF
• 一次／theorem-labs/oss-verify-proofs のREADME／収録ライブラリ数、定理の形、メモリ予算、LPSの限界、全体インデックスの件数
• 一次／theorem-labs/rocq-linux-process-semantics／RISC-VとLinuxプロセスのセマンティクス
• 二次／AiCybr ほか／発表側の数値（1.8億行、60万行、18,000命令、123ライブラリ・239エントリポイント、CVE-2026-56132、ワークスペース共有17%減）の独立確認

本記事は2026年10月23日時点の発表内容に基づき、公開リポジトリの数値は2026年10月29日に再確認しています。発表側の数値は一次ソースと二次ソースの双方で照合しました。本記事の筆者はイーランサー・ジャパンであり、取り上げた研究の当事者ではありません。