AnthropicがClaudeを活用し123個のオープンソースライブラリで形式手法による安全性検証を実現
AnthropicはTheoremと共同で、Claudeを用いてOSS-Fuzzのテストケースを仕様化し、123個のオープンソースライブラリでメモリ安全性を証明しました。約1.8億行のRocq形式の証明を生成し、大規模なソフトウェア検証の可能性を示しました。
AIが複雑なソフトウェアの安全性検証を自動化できることを示しており、将来的に商用ソフトウェアの脆弱性対策や品質保証プロセスを劇的に効率化する可能性があります。