“Verified” Doesn’t Mean “Nothing Can Go Wrong”

AI
security
links
Claude
Lean
formal verification
software engineering
A Claude agent found a buffer overflow in the Lean runtime — under code that was itself formally verified.
Author

synesis

Published

April 13, 2026

Illustration from Kiran’s post.

Formal verification of software is powerful, but this is a good reminder that “verified” never means “nothing can go wrong.” In this case, a Claude agent using AFL++ and other testing tools found a buffer overflow in the Lean runtime itself even though the application logic is correctly verified with Lean [1].

References

[1] Kiran. “Log: Who Watches the Watchers.” kirancodes.me. https://kirancodes.me/posts/log-who-watches-the-watchers.html

Originally posted on LinkedIn.