AnthropicがClaudeで形式検証を1億8000万行規模へ拡大
25秒でわかる内容解説
2026年10月22日、AnthropicはClaudeを用いた大規模な形式検証の結果を発表した。同モデルはRISC-Vアセンブリレベルで123のオープンソースライブラリを検証し、1億8000万行の証明コードを自動生成した。従来は専門家の手で作成に数年を要していた作業が、AIの自動化によって実用規模へ到達した。開発者はテストで見逃されたバグを修正し、安全性を数学的に保証できるワークフローが実現した。
Claudeが123ライブラリで自動証明を生成
Claudeが123のOSS-Fuzzライブラリを対象に形式検証を実行した。239のエントリポイントで検証に成功し、生成された証明コードは宣言型プログラミング言語Rocqで約1億8000万行に達する。典型的な証明は約60万行で、中央値1万8000命令のバイナリに対する安全性を保証する。
検証は単一スレッドの静的RISC-VバイナリをLinux上で動かす条件で行われた。64MB未満の入力に対してメモリ安全エラーやアサーション失敗がないことが数学的に証明された。
In order to prove a statement, the statement must correctly model the reality of the code.
命題を証明するためには、その命題がコードの現実を正しくモデル化する必要がある。
Claudeは発見したバグをコードにパッチを当て、再生成された仕様に対して再度証明を進めた。テストでは発見されなかったバグも多数特定された。その一つは10年以上潜伏していたロジックバグである。
新モデルOpus 5.5はOpus 5より約40%少ないトークンで検証タスクの半分を処理した。ファズテストが生成する膨大な半ランダム入力の様子が図示されている。 2026年10月22日付の発表で、AnthropicはAIによる形式検証の実用規模への拡大を示した。
証明はコンパイル済みのRISC-V命令上で動作し、Theoremが提供する命令セットとLinuxプロセスのセマンティクスを基に構築された。Rocqのチェッカーが仕様の正しさを保証するため、開発者が手動で確認する範囲は大幅に縮小された。
テストから仕様へ変換するパイプラインの確立
形式検証はコードを数学モデルに変換し、セキュリティルールに従うことを証明する手法だ。証明コードは元のコードの何倍にもなり、専門的なスキルを要するため実用性は限られていた。AnthropicとTheoremは既存のテストスイートを仕様に自動変換するパイプラインを開発した。Claudeはテストが常にパスするという仕様を生成し、バイナリレベルの証明を進めた。AddressSanitizerが検出するメモリ安全エラーも対象に含まれる。
OSS-Fuzzの数千の開発者作成エントリポイントを用い、fuzzerが生成する膨大な半ランダム入力を数学的に網羅する仕様へ変換した。モデルの能力向上に伴い、証明の作成コストは低下している。開発者が証明を共有・再利用する仕組みも導入された。
依存関係はべき乗分布に従うため、少ない共通ライブラリの証明で広範なソフトウェアの検証が可能になる。エージェントが作業を分け合う際、共通部分の証明をコピーすることでトークン数を17%削減できた。Mathlibのような共有ライブラリの成長パターンと同様に、検証コードベースが蓄積されれば実用性はさらに高まる。
依存関係の検証が1回完了すれば、それを利用する上位パッケージの検証コストは劇的に下がる。
実用性評価と仕様モデルの乖離を巡る議論
コミュニティは形式検証の実用性とバグ発見能力を高く評価している。一方で、生成された証明の複雑さがより大規模なプログラムで維持できるかは不明だ。仕様モデルが実際のハードウェアやOSの挙動を正確に記述できているかについても議論が交わされた。一部の開発者は、LLMが生成した命令型コードの検証よりも、宣言型言語への移行が進むと予測している。検証と検証の定義を巡る議論も見られる。
実際のデプロイ環境との乖離を埋めるために、x86やARM、glibcのセマンティクス生成が次の課題となる。検証対象の仕様が現実の要件を網羅できているかどうかも焦点だ。テストスイートから自動生成された仕様は、開発者の意図を完全に反映しているとは限らない。
このギャップを埋めるため、Claudeが仕様自体を生成・検証する実験も並行して進められている。形式検証が完了してもバグなしとは限らない。Claudeが書き上げた証明は外部のチェッカーで仕様の正しさを示すが、仕様そのものが現実の機械の挙動を完全に包み込めているかは別問題だ。
形式検証が実装レベルに普及すれば、テスト駆動開発に代わる堅牢な開発手法として定着する可能性が高い。
x86セマンティクス公開とNixエコシステム検証
現在の証明はRISC-Vとmusl libcを前提としている。実際のデプロイ環境であるx86やARM、glibcとの乖離を埋めるために、新しいシステムモデルの生成が進む。x86アーキテクチャのセマンティクス生成が次のステップとして進められている。TheoremはNixエコシステム全体の検証ロードマップを公開した。Claudeのスキルも公開され、開発者は自社のコードで検証パイプラインの実験を開始できる。
今後はglibcとの動的リンクやマルチスレッド環境への対応も予定されている。証明がカバーしない領域としては、未使用コードや呼び出し側のメモリ破壊が挙げられる。パブリック関数ごとの呼び出し規約を指定し、呼び出し側が厳密に遵守すれば、検証の範囲をさらに広げられる。
Anthropicは既存のソフトウェア資産を体系的に検証する戦略を提示した。NixエコシステムにはglibcやOpenSSL、cURLといった重要インフラが含まれ、依存関係の検証が完了すれば広範なソフトウェアの安全性が保証される。Theoremが公開したロードマップではパッケージ単位の検証が基盤となる。
x86セマンティクスが公開されれば、現在のRISC-V中心の検証環境はさらに拡張される。
用語の注釈
- Rocq
- 1980年代に開発された証明支援システム（旧Coq）。数学定理やプログラムの正しさを機械的に検証する宣言型プログラミング言語。（参考：Rocq（旧名 Coq）とは何か ── 「証明からプログラムを取り出す ...）