Anthropicは2026年10月22日、定理証明ツール企業Theorem Labsとの共同研究を通じ、Claudeを用いて123件のオープンソースライブラリ（239か所のファズテスト対象）のセキュリティ特性をRISC-Vアセンブリレベルで形式証明したと発表しました。デジタル庁が推進する政府情報システムや国内車載組み込みソフトウェアにおいて、従来の動的テストに依存した品質保証体制の再構築が求められます。
形式検証のコスト構造破壊とOSS Verifyの公開
AnthropicとTheorem Labsの研究チームは、AIモデル「Claude」を用いて約10億行の証明支援系言語Rocq（旧Coq）コードを生成しました。そのうち約1億8,000万行が証明チェッカーを通過し、オープンソースソフトウェア（OSS）の機械検証に成功しています。
検証対象となったバイナリの命令数中央値は18,000であり、典型的な1タスクあたりの証明コードは約60万行に達します。Theorem Labsはこの検証パイプラインを「OSS Verify」として無償公開し、開発者がGitHub経由で継続的検証（CI）に組み込める体制を整えました。
AI主導の脆弱性発見と検証自動化の時系列
ソフトウェアセキュリティの現場では、2026年に入りAIモデルによる脆弱性探索が急加速しています。今回の形式証明に至る背景には、脆弱性の発見速度に対して人間の修正が追いつかないという構造的要因が存在します。
| 年月 | 出来事 | 主な内容・影響 |
|---|---|---|
| 2026年8月 | Black Hat USA 2026 | AIによる脆弱性発見の急増が報告。Claude MythosがLinuxカーネル内で479件の脆弱性を検出。 |
| 2026年8月 | 米国政府「Gold Eagle」設置 | AI主導の脆弱性発見急増を受け、発見・緩和・修正を調整するクリアリングハウスを新設。 |
| 2026年9月 | 協調的開示プロセスの共同書簡 | Anthropic、OpenAI、AWS、Google、Microsoftなど100組織超が、修正プロセスの見直しを表明。 |
| 2026年10月8日 | 「OSS Scanner」提供開始 | AnthropicのFrontier Red Teamが、OSS向け脆弱性検出サービスを公開。 |
| 2026年10月22日 | 形式検証の共同研究成果を発表 | 123件のOSSライブラリに対するRISC-Vバイナリレベルでの形式証明と「OSS Verify」を公開。 |
従来の形式検証手法とのコスト比較
形式検証は、プログラムがあらゆる入力パターンに対して仕様通りに動作することを数学的に証明する技術です。しかし、人間が手作業で証明コードを記述する労力は極めて大きく、これまでは航空宇宙や防衛などの限定的な分野にとどまっていました。
| 検証プロジェクト | 対象規模 | 検証に要した工数・規模 | 検証コストの比率（実装比） |
|---|---|---|---|
| seL4（マイクロカーネル） | 約8,700〜10,000行のCコード | 20人年（person-years） | 実装工数（2人年）の約10倍 |
| 今回のClaudeによる検証 | 123ライブラリ（239エントリーポイント） | Claudeが約10億行生成、1.8億行が通過 | 超並列推論により数日から数週間で完了 |
2026年9月のMicrosoft「Patch Tuesday」では、1か月間で972件（うち112件がCritical）の脆弱性が修正されるなど、パッチ運用の負荷は限界に達しています。Anthropicの公式ブログが指摘するように、サイバー攻撃側の自動化に対抗するには、コードにバグが存在しないことを数学的に確定させるアプローチが必要とされています。
参考記事: AnthropicのAI、耐量子暗号「HAWK」の脆弱性を特定
バイナリ直接検証とエージェント推論の仕組み
今回の実証が成立した背景には、コンパイル後のバイナリを直接検証する形式意味論の設計と、推論モデルの協調動作があります。
コンパイラ最適化のバグを排除するRISC-V意味論
従来の形式検証の多くは、C言語などのソースコードレベルを対象としていました。しかし、ソースコードが正しくても、コンパイラの最適化処理によってメモリ破壊や未定義動作が混入するリスクを排除できません。
Theorem Labsは、RISC-V命令セットアーキテクチャ（ISA）およびLinuxプロセスの形式意味論をRocq上に構築しました。Googleの「OSS-Fuzz」環境で用いられるAddressSanitizer（ASan）組み込みバイナリを対象とし、コンパイル済みの静的バイナリを直接検証するパイプラインを採用しています。
開発者が信頼を置くべき要素（Trusted Computing Base: TCB）は以下の3点に限定されます。
- RISC-VおよびLinuxプロセスの形式意味論モデル
- 証明対象となる定理の数学的記述
- Rocqの証明チェッカー（カーネル）
この構成により、64MB未満のあらゆる入力とモデル化されたLinuxの全メモリ配置において、プログラムがAddressSanitizer違反やアサーション失敗を起こさないこと（クラッシュフリー性）が数学的に確定します。
深層バグの検出と探索空間の網羅
本プロジェクトでは、検証の過程で長年未発見だったバグが多数検出されました。従来のランダムファジングでは到達できない特定の境界条件が、形式証明の反証プロセスによって特定されています。
- 解凍プログラムの範囲外書き込み: 約20MBの入力において、極めてまれな特定のメモリ配置が発生した際にのみカウンターがアンダーフローする不具合。
- 画像デコーダーの範囲外読み取り: 64MBの入力と2GB以上のメモリ消費を同時に満たした条件下でのみ顕在化するバグ。
- 複数ハンドル操作時の不具合: 同一ファイルを指す2つのファイルハンドルに対し、特定の順序でAPI呼び出しを行った場合に生じるメモリ読み取りエラー。
- 重要アプリの未知ロジックバグ: クラッシュを伴わないため静的解析をすり抜けていた、ファイル読み込み制限機能の迂回バグ（10年以上潜在）。
Opus 5.5とエージェント間証明共有によるトークン効率
検証の実行フェーズでは、推論モデルの世代交代とマルチエージェント協調が計算資源の消費を抑えました。実際のOSS-Fuzzタスクを縮小した36件のベンチマークにおいて、以下の結果が得られています。
Opus 5.5は前世代のOpus 5と比較し、約40%少ないトークン数で課題の半数を証明しました。さらに、共有ワークスペースを介して互いの証明コードを再利用できるエージェント群は、単独動作のエージェントに比べて消費トークンを17%削減しました。C言語のランタイム初期化やASanコードなど、共通処理の証明をエージェント間でコピー・改変して適用する運用が機能しています。
前提条件（Prerequisites）と残る制約
本成果は広範な保証を提供する一方、商用環境における適用には前提条件の乖離が存在します。公開リポジトリ（theorem-labs/oss-verify-proofs）で初期公開された証明は25ライブラリ・60エントリーポイント（138件の証明記述）であり、以下の制約が明示されています。
- 実行モデルの制約: 証明は「単一スレッド」「固定メモリ量」「musl libc静的リンク」を前提としています。実運用の多くを占めるx86/ARM環境や、glibcへの動的リンク、マルチスレッド環境におけるデータ競合は検証の対象外です。
- 保証の範囲: 保証されるのは「クラッシュしないこと（crash-freeness）」であり、プログラムが無限ループに陥らず必ず終了する「停止性」までは証明されていません。
- 仕様と現実の乖離: Anthropic自身が言及している通り、証明チェッカーは形式仕様そのものが現実の物理ハードウェアやOSの挙動と完全に合致しているかまでは判定できません。
参考記事: 仕様駆動開発（SDD）の仕組みとは？バイブコーディングの限界と日立1,000人FDE体制が示す脱・人月のロードマップ
日本の産業構造におけるC言語資産とサプライチェーン検証
日本の産業界では、自動車制御、ファクトリーオートメーション（FA）、鉄道信号、医療機器などの組み込み領域において、膨大なC/C++コードが稼働しています。これらのミッションクリティカルなシステムに対し、今回の形式検証パイプラインは直接的な影響を与えます。
車載組み込み規格とファジング作業の再定義
車載ソフトウェアでは、ISO 26262などの機能安全規格に基づき、膨大な工数をかけてテストケースの作成とカバレッジ測定が行われています。しかし、どれほどテスト網羅率を高めても、複雑な入力空間におけるコーナーケースのバグをゼロにすることはできません。
Theorem Labsが「OSS Verify」を通じてglibc、OpenSSL、cURLを含むNixエコシステム全体の検証をロードマップに掲げていることは、ソフトウェアサプライチェーンの安全基準を根本から変えます。大手サプライヤーや完成車メーカー（OEM）にとって、採用するオープンソースコンポーネントに「Rocqによる形式証明が付帯しているか」が調達要件となる未来が現実味を帯びています。
国内企業における導入の構造的障壁
日本企業がこの検証手法を自社資産へ適用する上では、いくつかのハードルが存在します。
第一に、対象コードのモジュール構造です。検証パイプラインは明確なエントリーポイントと入出力制約を持つファズターゲットを起点としています。グローバル変数に強く依存した密結合なレガシーコードでは、形式仕様の記述自体が極めて困難になります。
第二に、形式手法を扱えるエンジニアの不足です。ClaudeがRocqコードを自動生成するとはいえ、TCBとなるRISC-V/OS意味論の妥当性を監査し、反証されたバグのパッチを承認する役割には、数理論理学と低レイヤーアーキテクチャの双方を理解する高度人材が不可欠です。
参考記事: AIセキュリティとは？NIST基準から学ぶ脆弱性対策と組織防衛の実践ステップ
ソフトウェア品質保証の移行に向けたアクション
テストによる確率的なバグ検出から、数学的証明による確定的保証への移行が始まっています。CTOおよび技術開発責任者は、自組織の開発パイプラインにおいて以下の取り組みを進めることが推奨されます。
- 基盤ライブラリのOSS Verify登録状況の確認
自社製品に組み込んでいる重要OSS（暗号、パーサー、プロトコルスタック）がTheorem LabsのロードマップやOSS-Fuzzに含まれているかを棚卸しし、検証済みパッチの追従プロセスを策定する。
- 自社C/C++コードのエントリーポイント分離とASan導入
AIによる形式検証を適用可能にする前提条件として、巨大なコードベースを独立したモジュールへ分割し、AddressSanitizerを用いたファズテスト環境をCI/CD上に構築する。
- ハードウェア意味論を意識したISA戦略の再検討
検証エコシステムが先行して立ち上がっているRISC-Vの動向を注視し、車載マイコンやエッジAI向けプロセッサの選定において、バイナリ形式検証の適用容易性を評価項目に加える。
出典: Unite.AI
出典: Anthropic
出典: Theorem Labs
出典: Kingy AI
