AnthropicとTheoremが連携、ClaudeがOSS-Fuzz収録123ライブラリのRISC-Vアセンブリでゼロクラッシュを初めて数学的に証明

2026年10月22日、AnthropicとTheoremは共同研究を発表した。ClaudeはGoogle OSS-Fuzz収録の123個の実在オープンソースライブラリを対象に、約1億8000万行のRocq証明コードを生成し、RISC-Vアセンブリレベルで239のエントリポイントについて「任意の入力でクラッシュしない」ことを数学的に証明した。

事実の整理

研究によると、Claudeはシングルスレッドの静的バイナリ、固定メモリ予算のRISC-V CPUおよびLinux OSという前提条件のもとで、プログラムが常に正常終了し、メモリ安全エラーやアサーション失敗を引き起こさないことを証明した。入力の上限は64MBとされている。このプロセスにおいて、数兆回のファジングテストでも発見されなかった隠れた脆弱性も複数検出された。研究では証明コードの一部およびRISC-VとOSのセマンティクスが公開されており、Theoremは同一のワークフローを他のオープンソースプロジェクトでも利用できるよう提供するとともに、開発者の導入を支援するClaude向けスキルも公開した。

メカニズムの解説

形式検証はまずコードを数学的モデルに変換し、それが既定の安全規則を常に満たすことを証明する。証明に失敗した場合、規則違反の可能性がある脆弱性を特定し、原因を排除した後に再度プロセスを繰り返すことで、最終的に違反のない証明を得る。従来、証明コードの量は元のコードをはるかに超えており、高度な専門スキルを要していた。例えばseL4カーネルの実装には2人年しかかからなかったのに対し、検証には20人年を要している。今回Claudeが証明を自律生成したことで、このプロセスが量産可能な自動化パイプラインへと進化した。

産業への影響

この取り組みは形式検証の適用範囲を、従来の任務クリティカルなアプリケーション（エアバスの航空電子コードなど）に限定された領域から、より広範な実在オープンソースライブラリへと拡大した。証明の再利用・修正が可能であることから、後続のコードベースにおける検証コストの分散が期待される。Theoremのパイプラインサービスとスキルの公開は、開発者に直接的な導入経路を提供する。モデルの性能向上に伴い、形式検証はセキュアなソフトウェア開発における標準的な構成要素となる可能性がある。

戦略的見解

（考察であり事実ではない）本研究はモデルの長期推論能力、コード理解能力、および論理証明能力を同時に試すものであり、既存のコード実行や複雑推論の定量評価と対を成すものである。ベンチマークのスコアにとどまらず、AIの実際のエンジニアリングにおける約束遵守能力が検証可能な形で顕在化しつつある。モデルが継続的に改善されれば、証明コストの低下がセキュリティ保証の標準化を加速させるだろうが、あらゆる潜在的脆弱性の網羅的な排除にはさらなる探求が必要である。