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.

​Register for the in-person event

​Please register to reserve your seat at the in-person event. We’ll provide lunch for everyone registered and we'll send you the precise venue address closer to the date.

​Join the waitlist to watch the livestream

​If registration is full, join the waitlist. Everyone on the waitlist will receive a livestream link before the event, and recordings will be available afterward.

​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!