Anthropic、Claudeが123のオープンソースライブラリ向けにアセンブリレベルの形式証明を生成したと発表

Anthropicは、形式検証企業のTheoremと提携し、オープンソースプロジェクトの既存ファジングテストを数学的仕様に変換し、Claudeが証明を作成してRocq証明チェッカーで検証する体制を構築した。Anthropicによると、チームは数週間で123のオープンソースライブラリと239のテストエントリポイントに関する証明を完了し、証明コードの合計は約1億8000万行に達した。主要な結論は、入力サイズが64 MB未満であり、設定されたLinux応答およびメモリレイアウトの条件下において、パッチ適用後に特定のRISC-Vプログラムとしてコンパイルされたテストエントリポイントは、メモリセーフティエラーやアサーション失敗によってクラッシュしないというものである。Claudeは証明作成中に、従来のテストでは検出されなかった問題、特に稀な入力でしか発生しないバウンダリ外読み書きも発見し、パッチを適用した。反復サンプリングによるファジングと比較して、形式的証明は定義された範囲内のすべての入力を網羅できるが、結論は仕様、マシンモデル、およびチェッカーの正確性に依存する。現在、主要な証明はシングルスレッドや静的リンクといった特定の動作環境を対象としており、各ライブラリの全コードをカバーしているわけではない。Anthropicは一部証明を公開し、外部による検証と再利用を可能にしている。本研究は、AIが形式検証の作業負荷を低減する可能性を示すものだが、これをもって123のライブラリが「脆弱性なし」と断定することはできない。