目次
AIがコードを生成し、別のAIがレビューする流れは広がりました。そこへ「AIが安全性を数学的に証明する」という選択肢が加わりつつあります。ただし、証明という言葉だけを見て、対象ライブラリ全体が安全になったと判断するのは危険です。
Anthropicは2026年10月22日、Claudeと形式手法を使い、Google OSS-Fuzzに登録された123のオープンソースライブラリについて、239のファズテスト入口で「指定された条件内ではクラッシュしない」ことを機械検証したと公表しました。証明はソースコードではなく、RISC-V向けにコンパイルした実行バイナリを対象としています。
本記事は同日公開の研究記事、公開された証明リポジトリ、Linuxプロセスの形式モデルを2026年10月25日に確認したトレンド分析です。研究チームの主張と公開成果物から確認できる範囲を分け、Web開発チームが導入判断に使える形で整理します。本サイトで同じ証明を再実行した結果ではありません。
スポンサーリンク
形式検証は大量のテストとは役割が違う
ファジングは、多数の入力を実際に与えてクラッシュや異常を探します。長く動かすほど多くの経路を試せますが、可能な入力をすべて実行することはできません。形式検証は、プログラムと実行環境を数学的なモデルへ置き換え、定義した性質が対象範囲のすべての入力で成り立つことを証明します。
今回の研究では、既存のOSS-Fuzz用ハーネスを仕様の起点にしました。ハーネスが異常時に停止するよう作られていれば、「どの対象入力でもその停止に到達しない」という定理へ変換できます。ClaudeがRocq用の証明を書き、Rocqのカーネルが定理と証明の整合性を機械的に確認する構成です。AIの回答を人が信用して採用する方式ではありません。
Anthropic：LLMs are making formal software verification feasible at a much larger scale
今回証明したのは指定入口の無クラッシュ性
Anthropicの説明では、入力が64MB未満で、単一スレッドの静的バイナリがRISC-V CPUとモデル化されたLinuxプロセス上で動き、固定したメモリ予算に収まることなどが前提です。その条件内で、AddressSanitizerが検出するメモリ安全性違反やアサーション失敗へ到達しないことを対象にしています。
これは重要な保証ですが、次の主張とは異なります。
- 対象ライブラリの全機能に脆弱性がない
- x86-64やARM、動的リンク、本番のglibc環境でも同じ結果になる
- 認証やアクセス制御など、ハーネスに表現されていない論理要件が正しい
- 処理が必ず終了し、サービス拒否やメモリ枯渇が起きない
- 呼び出し側がAPIを誤用しても安全である
公開リポジトリも「ライブラリが正しいとは言わない」「一つの入口から到達するコードが対象」「終了しない実行は排除しない」と明記しています。証明済みというラベルを依存パッケージ全体の免責へ読み替えないことが、導入時の最初の判断です。
スポンサーリンク
研究全体と公開リポジトリの数字を混同しない
Anthropicの研究記事は、123ライブラリの239入口で証明に成功し、証明コードは約1億8000万行に達したと報告しています。一方、確認時点の公開リポジトリには、25ライブラリの60入口について証明が掲載されています。さらにリポジトリの状態表には、2148ハーネスに対する2万164個の定理文のうち、138個が証明済みと記録されています。
数字が食い違うのではなく、研究全体と公開された再確認可能な部分の単位が異なります。未修正の問題を明らかにする可能性がある証明は公開しない方針も示されています。導入検討では、研究記事の集計だけでなく、自分が評価したい依存関係・入口・ビルド条件の成果物が公開されているかを確認してください。
Theorem Labs：OSS Verifyの証明リポジトリ
証明を信頼する範囲にも境界がある
機械検証では、長大な証明を一行ずつ人が読む必要はありません。その代わり、何を定理として記述したか、実行環境のモデルが現実をどこまで表すか、証明チェッカーが正しく動くかを信頼する必要があります。今回ならRocq、LPSと呼ばれるLinuxプロセスモデル、RISC-Vバイナリをモデルへ取り込むツール、許可された公理などが信頼境界です。
本番サーバーがx86-64、動的リンク、複数スレッドで動いているなら、公開証明と実環境の差を記録します。証明対象のコミットと、自社のロックファイルやコンテナに入った版が同じかも別の確認です。証明が正しくても、別のビルドや更新後のバイナリへ自動的に引き継がれるわけではありません。
Theorem Labs：Rocq Linux Process Semantics
スポンサーリンク
AIが修正したコードは別のレビュー対象になる
証明の途中で反例が見つかると、Claudeはコードを修正してから証明を続けました。この自動化には注意点があります。定理を通しやすくするために、本来の機能を削る、入力を拒否する、到達経路を変えるといった修正をすれば、形式上は証明できても製品要件を壊す可能性があります。
Anthropicは、変更を罰する評価や、どの入力の挙動を変えたかを証明する追加点、パッチの監査を用いたと説明しています。それでも、採用側は「証明が通った」と「意図した機能が保たれた」を別のゲートにしてください。API互換性、既存テスト、性能、エラー処理、ライセンス、上流プロジェクトのレビューを省略できません。
AIレビューの検出数や費用を比較するときも、評価条件の確認が必要です。既存記事のAIセキュリティレビューは安さだけで選べない？Cloudflareの改善報告から考える検証では、指摘をそのまま成果と数えない評価方法を整理しています。形式証明では、指摘の確認に加えて定理と前提の確認が中心になります。
Web開発チームは高リスクの入口から試す
研究結果を見て、すべての依存パッケージを直ちに形式検証するのは現実的ではありません。今回の公開手順では、一つの証明確認に16コアで最大20GiBのメモリを使う場合があるとされています。Anthropicも、証明生成には数億トークン規模を要し得ることを制約として挙げています。
本サイトでは、外部から受け取る非信頼データをネイティブコードで解析する入口から候補を選ぶ方法を提案します。画像、圧縮データ、JSON、TLS、証明書、HTTPなどのパーサーは、Webサービスの入力境界に置かれやすい領域です。ただし、公開リポジトリに対象があるだけで採用せず、自社が呼ぶ関数と証明済みハーネスの到達範囲を照合します。
- SBOMやロックファイルからネイティブ依存関係と実版を出す
- 外部入力から依存関係までのデータ経路を特定する
- 守りたい性質を「クラッシュしない」「特定の往復変換が一致する」など具体化する
- 既存のファズテストがその性質を失敗として表現しているか確認する
- 証明対象の入口・コミット・CPU・OS・リンク方式・入力上限を記録する
- 証明と並行して、実環境でのファジング、回帰テスト、監視を継続する
CIへ入れるなら生成と確認を分ける
AIに証明を生成させる工程は、長時間・高コストであり、外部サービスや大きな計算資源を使う可能性があります。一方、完成した証明を固定したチェッカーで再確認する工程は、リリース判定へ組み込みやすくなります。公開リポジトリも、バイナリのSHA-256確認、証明のコンパイル、許可されていない仮定の拒否を同じチェック手順で実行しています。
本サイトでは、証明生成環境に本番秘密情報を置かず、対象ソースとテスト、固定したツールチェーンだけを渡すことを勧めます。生成されたパッチは通常のプルリクエストへ戻し、人の承認と既存CIを通します。証明確認用コンテナはダイジェストで固定し、ネットワークを無効化し、証明・定理・バイナリ・ビルド記録を同じリリース成果物として保存します。
AI機能の変更を継続的に判定する土台は、AIの改善を勘で判断しないために｜評価データと回帰テストの始め方で扱っています。形式検証を追加しても、ユーザー要件や業務上の正しさを測る評価セットは残ります。
導入判断では保証の文をそのまま書き出す
「形式検証済み」という短い表現では、社内レビューや顧客説明で保証範囲が膨らみます。採用記録には「どのバイナリの、どの入口について、どの入力範囲と実行モデルで、どの失敗を排除したか」を一文で書きます。証明がカバーしないCPU、OS、スレッド、終了性、論理要件、呼び出し側の誤用も併記します。
今回の成果は、AIが書いたコードをAIが雰囲気で採点する仕組みではなく、外部の小さな検証器へ通る数学的証明を大量に作った点に価値があります。同時に、仕様と環境モデルの外側は保証されません。Web開発チームにとって当面の現実的な使い方は、置き換え可能な既存テストを捨てることではなく、攻撃面が大きい入口に限定して、ファジングでは到達しにくい経路へ追加の保証を置くことです。
スポンサーリンク
依存関係の更新後は証明の鮮度を確認する
証明は特定のバイナリとコミットへ結び付いています。ライブラリを更新したとき、脆弱性修正を取り込んだとき、コンパイラーやリンク設定を変えたときは、以前の証明をそのまま適用しません。変更差分に関係する入口の定理を再生成し、同じチェッカーで確認します。緊急更新では証明の完了を待って修正を遅らせず、先に安全版へ更新し、ファジングと回帰テストを実施したうえで追加保証を追随させる順序が現実的です。
また、上流が公開した証明を利用する場合は、証明ファイルだけでなく、対象バイナリの由来、ビルド記録、ハッシュ、チェッカーのイメージダイジェストをそろえて取得します。証明の配布経路が改ざんされれば、検証対象そのものを取り違えるためです。
