Appearance
Software Verification in Lean2026
Advancing software correctness with Lean
Skip to content
Registration
Registration is free but mandatory. You can register using this form. Please note that room capacity is very limited. Talks will be streamed — more details will appear on this website in due time.
About
Software Verification in Lean is a one-day open workshop dedicated to the formal verification of software using the Lean 4 theorem prover. The workshop brings together researchers and practitioners to share recent advances, practical techniques, and ongoing challenges in building verified software. Whether you work in proof engineering, programming language theory, or software development, we invite you to join us for a day of talks and discussion.
Schedule
| Time | Speaker | Title |
|---|---|---|
| 10:00–11:00 | Leo de Moura | To be announced |
| 11:00–11:30 | Coffee break | |
| 11:30–12:30 | Son Ho | To be announced |
| 12:30–14:00 | Lunch break | |
| 14:00–15:00 | Derek Sorensen | Correct and Computable Specifications in LeanThe efficacy of formal verification depends on high quality specifications which are both correct and complete. This talk will ask: What is an ideal specification? How do we evaluate and improve our specifications? And how can Lean help us achieve the highest-assurance software possible? |
| 15:00–15:30 | Coffee break | |
| 15:30–16:30 | Karthikeyan Bhargavan | To be announced |
Organizing Committee
Venue
Organized by
Partners