Software Verification in Lean2026 · Fall

About ​

Co-organized by the Beneficial AI Foundation and the Lean FRO, Software Verification in Lean brings together researchers and practitioners working on formal verification of software using the Lean theorem prover. The Fall 2026 edition follows the first SVIL event, held in Paris earlier this year.

This edition is a day of public lectures on advancing Lean’s software verification ecosystem toward production use, with a focus on end-to-end verification of security-critical systems and BAIF’s Secure Stack initiative. The talks will address gaps in low-level verification, usability, and performance, and bring tool developers and users together with Lean developers.

Speakers ​

• Max Tegmark and Shaowei Lin (Beneficial AI Foundation)
• Leonardo de Moura (Lean FRO)
• Jonathan Protzenko (Google)
• Mike Dodds (Oath FRO)
• Andres Erbsen (University of Washington)

Program ​

A one-day program of talks on Saturday, November 7, 2026, from 9:30 AM to 5:00 PM Pacific Time. Each talk is followed by a discussion. Talk titles to be announced closer to the event.

Registration ​

Registration is required and subject to host approval. Find more details and request to join on Luma.

Venue ​

Stanford University

Organizing committee ​

Organized by ​