Software Verification in Lean: Palo Alto 2026

​SVIL is a one-day, in-person series of public lectures on applying Lean to software verification. Space is limited, and registration is required.

​Join the waitlist to watch the livestream

​Everyone on the waitlist will receive a livestream link before the event, and recordings will be available afterward.

​The in-person event

​The in-person event is now full. Please join the waitlist to receive a link to the livestream.

​About the talks

​Co-organized by the Beneficial AI Foundation and the Lean FRO, SVIL presents the progress BAIF and the Lean FRO are making to improve Lean’s software verification infrastructure. The talks focus on:

• ​Rust verification with the Aeneas framework

• ​Low-level software verification

• ​Formally verified OS kernels

​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

​We look forward to seeing you at the event!