コード生成後の検証も自動化へ
Anthropicは2026年10月22日、Theoremと協力し、Claudeを使って123のオープンソースライブラリの特定の安全性を証明したと発表しました。既存のファジング用テストを仕様に変え、生成した証明を外部の証明検査器で確認します。失敗例を探すだけでなく、定義した条件で安全性を示す研究です。
対象は単一スレッドの静的RISC-Vバイナリ、モデル化したLinuxの動作とメモリ条件、64MB未満の入力などに限定されます。すべての入口やライブラリ全体を網羅したわけではなく、通常のx86・ARM環境へ保証をそのまま移せません。研究実施者の報告であり、公開される証明も一部です。
正しい証明にも適切な仕様が必要
開発者には、完了条件をテスト通過から明示的な性質へ広げる動きとして重要です。ただし検査器は、仕様が現実の要求を十分に表すかまでは保証しません。入力範囲、実行環境、呼出側の義務を確認し、依存関係や配備先が変われば再検証すべきです。全バグの解消や安全確認の省略を認める発表ではありません。