AI, Lean, and the Future of Formal Verification, with Lean Creator Leo de Moura

Leo de Moura, creator of Lean and an AWS research leader, argues that as AI makes code generation easier, proving that generated software meets its requirements becomes a central challenge. Lean is both a programming language and a proof assistant: developers state properties and provide proofs that a small checking kernel can verify. Unlike testing, which can reveal bugs but cannot establish their absence, machine-checked proofs can demonstrate that an implementation satisfies a specified property. Examples include a Lean port of the zlib compression library proving that decompression restores the original data, and Aeneas, which supports verification of Rust code and is used with Lean on Microsoft’s SymCrypt cryptography library. AI is also accelerating the translation of mathematics and programs into formal proofs, producing work far larger than human-built libraries such as Mathlib.

That progress does not eliminate the need for human judgment. When AI translates existing software into a Lean model, the model may not faithfully represent the original code; differential testing can expose mismatches and help find real bugs, but a proof is only as meaningful as its model and specification. Establishing that software is bug-free therefore requires checking the requirements, validating the formalization, and keeping it aligned with the implementation. De Moura expects engineering to focus increasingly on specifications and properties rather than code alone, with formal methods helping assess AI-generated systems and autonomous agents. The discussion also considers AI-assisted mathematics and possible applications beyond software, including physics, finance, chemistry, accounting, and law.