Anthropic、Claudeで123のOSSライブラリを形式検証
AnthropicはTheoremと共同で、Claudeを使いOSS-Fuzz登録の123ライブラリの安全性を検証し、239件の証明を完了したと発表した。
Anthropicは2026年10月22日、形式証明の専門企業Theoremと共同で、GoogleのOSS-Fuzzプロジェクトに登録されている123のオープンソースライブラリについて、Claudeを使ってセキュリティ特性を形式検証したと発表した。aitimes.comが報じた。
Claudeは123ライブラリの239のテストエントリーポイントに関する証明を完了し、64MB未満のあらゆる入力に対してテストがクラッシュせずに終了すること、メモリ安全性エラーやアサーション失敗が発生しないことを示した。生成された証明はRocq形式で合計1億8000万行に達し、証明の中央値は約1万8000のRISC-V命令からなるバイナリを対象とした。
証明の過程でClaudeは数百のバグを発見し、コードを修正して再証明した。例として、解凍器のカウンタ・アンダーフローや画像デコーダの範囲外読み取りが挙げられている。また、libexpatのXMLパーサーライブラリにおけるCVE-2026-56132も再発見した。
Anthropicは、アセンブリコードレベルで本番ソフトウェアのセキュリティ特性を大規模にAI検証したのは今回が初めてだとしている。証明の一部と検証に使用したモデルは公開され、Theoremは同じプロセスを他のオープンソースプロジェクトに適用するための支援を提供している。
別実験ではOpus 5.5がトークン効率改善
別の実験では、Opus 5.5が36件の検証タスクのうち半数を、Opus 5より約40%少ないトークンで解決した。エージェント間の協調によりトークン使用量は17%削減された。
よくある質問
Claudeは何件のライブラリを検証しましたか？
OSS-Fuzzに登録された123のオープンソースライブラリで、239のテストエントリーポイントの証明を完了しました。
生成された証明の規模はどれくらいですか？
Rocq形式で合計1億8000万行に達し、証明の中央値は約1万8000のRISC-V命令からなるバイナリを対象としています。
Opus 5.5の実験結果は？
36件の検証タスクの半数をOpus 5より約40%少ないトークンで解決し、エージェント協調でトークン使用量が17%削減されました。