Lean でプログラムの正しさを証明した。そしてバグを見つけた

記事

• 著者が Lean 4 で圧縮アルゴリズムを形式検証した
• バグを2件発見——いずれも証明の境界外: DoS（仕様のギャップ）と Lean 自体のヒープオーバーフロー
• AI支援ファジング（自動的にランダム入力を投げてバグを探す手法）で Lean ランタイムのヒープオーバーフローを発見

ディスカッション

• タイトルは誤解を招くとの指摘: 証明済みコードにバグはなく、バグは未検証のパーサーとランタイムに存在した
• 重要な洞察: 証明はその適用範囲内でのみ成立する。境界こそが破綻する場所
• Lean 自体のヒープオーバーフローをファザーが発見した点が本当の読みどころとの声
• Knuth の言葉が引用された: “I have only proved it correct, not tried it”（「正しいことを証明しただけで、実際に試してはいない」）

HN で議論する

原文（英語）: Lean proved this program correct; then I found a bug