I'm a Senior Principal Applied Scientist in the Automated Reasoning Group at AWS. I'm also the Chief Architect and co-founder of the Lean FRO, a non-profit organization dedicated to the development of the Lean theorem prover and programming language.
My research areas are automated reasoning, theorem proving, decision procedures, SAT and SMT. I am the main architect of Lean and Z3. Recipient of the Herbrand and CAV awards, and the ACM SIGPLAN Software Award for both Z3 and Lean.
Current Work
-
Lean Theorem Prover and Programming Language — expressive types, powerful automation, a programmable ecosystem
-
grind — a Lean tactic inspired by modern SMT solvers, combining E-matching, congruence closure, and linear arithmetic
-
sym — a new framework for building scalable software and hardware verification tools in Lean
Recent Writing
-
Who Watches the Provers? — why Lean's multi-kernel architecture survives AI-scale adversarial pressure
-
Teaching AI to Make Proof Automation Work — a research challenge for the ML community
-
When AI Writes the World's Software, Who Verifies It? — the case for verified software at AI scale
-
Proof Assistants in the Age of AI — why proof assistant design matters more, not less