Lean proved this program was correct; then I found a bug.13 Apr, 2026   lean formal_verification security fuzzing I fuzzed a verified implementation of zlib and found a buffer overflow in the Lean runtime. AI agents are getting very good at finding vulnerabilities in large-scale software systems. Anthropic, was apparently so spooked by the vulnerability-discovery capabilities of Mythos, they decided not to release it as it was "too dangerous" (lol). Whether you believe the hype about these lates...