Leo de Moura says AI agents are making formal verification practical

However, he emphasizes that AI-generated models of code must be verified for faithfulness to the original source. He points to a recent example where Claude Code found real bugs in its own codebase using Lean, but notes that proving the absence of bugs still requires human oversight of the specifications and models. The conversation also touches on the Navier-Stokes equation proof, where mismatches between informal and formal proofs highlighted the need for better tooling like Verso Blueprint to align natural language and Lean code.