Anthropic、Claudeがオープンソースライブラリ123件がクラッシュしないことを形式的に証明したと発表

Theoremとの共同作業で、AnthropicはClaudeを使い、100件を超える実世界のオープンソースライブラリについて、アセンブリレベル（RISC-V）でセキュリティ特性を証明したと発表した。同社はこれを、このレベルでAIを使って本番ソフトウェアを形式検証した初の大規模な事例と呼んでいる。

Anthropicによると：

• 証明された内容： OSS-Fuzzのライブラリ123件にあるファズテストのエントリポイント239件について、64 MB未満のあらゆる入力で、プログラムが常に正常終了し、メモリ安全性エラーやアサーション失敗がないことを証明した。これは、Linuxを実行するRISC-V CPU上で、単一スレッドの静的バイナリが固定のメモリ予算で動作するという前提のもとで成り立つ。証明は合計約1億8000万行のRocqに及び、Rocqの証明チェッカーで検証された。
• 方法： 各ライブラリに既存のファズテストを仕様（「このテストは決してクラッシュしない」）に変換し、Claudeが証明を作成する過程で、見つかったバグにパッチを当てた。Anthropicによると、これにより何百件ものバグが見つかった。ファザーでは見つけにくいと考えられる、まれな20 MBの入力を必要とする範囲外書き込みや、libexpatにおけるCVE-2026-56132の再発見などが含まれる。
• その他の実験： Claudeは、Linuxカーネルのzlib実装がx86バイナリレベルでRFC 1950の仕様に一致することを証明し、さらに、動作がCPythonと170万件のランダムなプログラムの99.95%で一致するRust製のPythonインタプリタを構築した。Anthropicによると、広く使われているPDFリーダーに形式検証を試みたところ、通常1年間に報告されるのと同数のセキュリティバグが1週間で見つかった。
• コスト： 証明には数億トークンかかることがある。Anthropicによると、36件の小規模な検証タスクでは、Opus 5.5はOpus 5より約40%少ないトークン数で半数を証明し、証明を共有するエージェントは必要なトークン数を17%削減した。

Anthropicは証明の一部と、RISC-VおよびLinuxのセマンティクスを公開している。Theoremは他のオープンソースプロジェクトでも同じパイプラインを実行すると申し出ており、自分のコードを検証するためのClaude skillを公開している。Anthropicは、これがライブラリにバグがないことを示すものではなく、残るバグは信頼されたコンポーネント内、または証明の対象範囲外にあると指摘している。