Leonardo de Moura

Cray Colloquium at the University of Minnesota

Next Monday, I am giving the Cray Distinguished Colloquium at the University of Minnesota Department of Computer Science & Engineering. The Cray Colloquium Series was founded more than 30 years ago with a donation from Cray Inc. to honor the contributions and legacies of Dr. Seymour Cray. Past speakers include Turing Award winners and members of the National Academy of Engineering.

The talk covers the convergence of formal verification and AI: how Lean became the platform every AI math system trains on, what machine-checked proofs mean for software reliability, and where proof automation is heading. It includes live demos of grind, the Radix verified DSL built by 10 AI agents in a weekend, and examples from Cedar, SymCrypt, and Veil.

Slides