形式検証ツール「Lean」がバグゼロを保証したzlibの実装に、実際にはバッファオーバーフローが存在したことが判明した。研究者がファジングを用いてlean-zipを検査したところ、Leanランタイム内のバグを発見。「証明済み＝安全」という前提が崩れた。
ことの発端は、10体のAIエージェントが自律的にzlibの検証済み実装「lean-zip」を構築・証明したという注目の成果。Lean FROの主任設計者レオ・デ・モウラも絶賛したエンドツーエンドで正確性が保証されたはずの実装だったが、形式証明が対象にできるのはあくまで仕様の範囲内に限られる。
今回の件は、形式検証はバグを根絶する「銀の弾丸」ではないという現実を改めて示した。AIによる脆弱性発見コストが急落している現在、形式検証への過信は新たなリスクを生む可能性がある。ソフトウェアセキュリティの根本的な再考が求められている。
