1. 【最重要】Anthropic、Claudeで123のOSSライブラリを形式検証 — 約1億8,000万行の証明を生成
発表：10月22日｜新研究・検証コード公開
Anthropicが、形式検証企業Theoremとの共同研究を発表しました。
Claudeを使い、123のオープンソースライブラリに含まれる239のテスト用エントリーポイントについて、特定の条件下でクラッシュしないことを数学的に証明しています。
対象はコンパイル済みのRISC-Vバイナリで、生成した証明はRocqという形式的証明システムで検証されました。証明の過程では、従来のファジングで長年発見されなかった不具合も検出しています。
なぜ重要か
従来のテストは、有限個の入力に対して正しく動くことを確認する方法です。
今回の技術は、定義した条件を満たすすべての入力について、特定の不具合が発生しないことを証明するものです。
技術・実装ポイント
| 項目 | 研究結果 |
|---|---|
| 対象ライブラリ | 123 |
| 検証したエントリーポイント | 239 |
| 証明コード | 約1億8,000万行 |
| 典型的な証明の規模 | 約60万行 |
| 入力サイズ | 64MB未満 |
| 対象アーキテクチャ | RISC-V |
| 証明システム | Rocq |
仕組みは次のとおりです。
text既存のOSSライブラリ
↓
OSS-Fuzzのテスト
↓
形式的な仕様へ変換
↓
Claudeが証明を生成
↓
Rocqが数学的に検証
↓
証明失敗時は不具合を調査
↓
必要に応じて修正・再証明性能： Claude Opus 5.5は、36件の小規模検証課題において、Opus 5より約40%少ないトークンで半数の課題を証明しました。
コスト： 大規模な証明には数億トークンを必要とする場合があり、一般的なCIへそのまま導入するには費用面の課題があります。
利用条件： 証明の一部、RISC-VとOSの形式的モデル、開発者向けClaude Skillが公開されています。
重要な制限： 今回の証明は、単一スレッド、静的リンク、固定メモリ予算などを前提としています。x86やARMで実行するすべての構成について安全性が保証されたわけではありません。
特に注目したいのは、AIが証明を生成し、その正しさはAIではなく独立した証明器が判定していることです。