Leonardo de Moura

Leonardo de Moura is a computer scientist, and creator of the Z3 Theorem Prover and the Lean proof assistant during his time at Microsoft Research. He currently works at AWS and is the Chief Architect at the Lean FRO.

Awards and honors

The 2007 CADE Skolem Award for the paper "Efficient E-Matching for SMT Solvers" that has passed the test of time, by being a most influential paper in the field.
The 2021 Computer Aided Verification Award for the field-changing contributions regarding his work on Z3.
The 2025 CADE Skolem Award for the paper "The Lean Theorem Prover " that has passed the test of time, by being a most influential paper in the field.
The 2025 ACM SIGPLAN Programming Languages Software Award for his work on Lean.