北京時間 2026 年 10 月 23 日およそ 06:01、Anthropic 公式アカウントは X で、日付が 2026 年 10 月 22 日の Frontier Red Team 研究記事を案内した。Anthropic によれば、Theorem との協力で Claude が Google OSS-Fuzz 由来の実在オープンソースライブラリに対し、RISC-V アセンブリ層でセキュリティ性質を形式証明したという。DigIntoAI は証明もパイプラインも実測していない。
Anthropic によると、Claude は発見した不具合を修正したうえで、123 の OSS-Fuzz ライブラリにわたる 239 の fuzz 入口点について、64MB 未満の任意入力およびモデル化した Linux OS 応答・メモリ配置のもとで、メモリ安全性エラーやアサーション失敗によるクラッシュが起きないことを証明した。Anthropic は自社の知る限り、生産ソフトウェアに対するアセンブリレベルでの AI 形式検証を大規模に行った初の取り組みだと述べる。一部の Rocq 証明と信頼コンポーネントを公開し、Theorem は他のオープンソース向けに同パイプラインを提供し、開発者が始めやすい Claude skill も公開するとしている。
Anthropic は境界も明示する。証明の前提は単一スレッドの静的バイナリ、固定メモリ予算、RISC-V CPU、Linux である。信頼対象は RISC-V と Linux プロセスの形式モデル、証明した定理の文言、Rocq 証明検査器だ。これでライブラリにバグが無いことにはならない、と Anthropic は書く。残る問題は信頼コンポーネント内か、証明範囲外にあり得る。要するに、LLM で規模化した形式検証は、これらの仮定のもとで述べられた非クラッシュ仕様を証明できるが、あらゆる配備でゼロバグを単独保証するものではない。関連する DigIntoAI 記事は Anthropic の Claude による攻撃対象領域縮小、Anthropic の Agent Skills の AAIF 寄贈、METR と Redwood が OpenAI の社内 agent 監視をレッドチーム評価 を参照。
Rocq 証明の再現、当該 OSS-Fuzz 入口点の再実行、Theorem の Claude skill の確認はいずれも行っていない。
