https://kirancodes.me/posts/log-who-watches-the-watchers.html
Article
-
Author formally verified a compression algorithm in Lean 4
-
Found two bugs — both outside proof boundaries: a DoS (spec gap) and heap overflow in Lean itself
-
Used AI-assisted fuzzing to discover the heap overflow in Lean’s runtime
Discussion
-
Title disputed: proven code had no bugs; bugs were in unverified parser and runtime
-
Key insight: proofs only hold within their operating envelope; boundaries are where things break
-
Fuzzer finding a heap overflow in Lean itself called the real story worth attention
-
Knuth quote invoked: “I have only proved it correct, not tried it”
Discuss on HN