Lean@Google 2025

The ISE Formal team at Google will meet with Lean experts to advance the state of program verification, from Dec 15th to Dec 19th, in Seattle.

Program: Livestreamed Keynotes

The first half-day will consist of publicly-available livestreamed keynotes on Dec 15th.

• 8am-9am: Leo de Moura, “State of Lean”

• 9am-10am: Sebastian Ullrich, “Optimizing Lean Libraries using the Module Systems”

• 10am-11am: Théophile Wallez, “Proofs of Security Protocols in Lean”

• 11am-12pm: Son Ho, “Proving Rust programs in Lean with Aeneas”

The talks will be livestreamed on Google Meet.

Program: Internal Hackathon

The rest of the week will be internal to Google; broadly speaking, the agenda is to:

• discuss Lean issues surfaced by the Aeneas project (Rust verification) and the Bob DyLean project (symbolic proofs of protocol security in the Dolev-Yao model)

• increase ISE Formal's fluency in Lean

• come up with a set of program verification challenges in Lean, notably around linear arithmetic and the kinds of proofs found in cryptography / security verification

• establish some new grand challenges for program verification

• strengthen our ties with the Lean community

Googlers are welcome to reach out to protz@google.com if they are interested!

Expect a blog post on my blog in the new year to summarize the outcomes of the week.