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. We have reached maximum on-site capacity — attendance is now online only. A link for the streaming will be sent to registered participants shortly before the talks start.
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 |
|---|---|---|
| 9:00–10:00 | Max Tegmark and BAIF | Open tools and standards for scaling software verification |
| 10:00–11:00 | Leo de Moura | Scalable Software Verification in Lean 4Lean 4 is evolving from a theorem prover into a platform for scalable software verification. A key challenge is closing the performance gap between Lean's automation and the tools used in software verification (e.g., Aeneas, mvcgen, Velvet). In this talk, I presentSymM, a new monadic framework designed for high-performance software verification tools built on top of Lean. SymM enforces a monotonically growing local context, enabling cheap definitional equality checks, optimized introduction and application tactics, and efficient rewriting—all while sharing infrastructure with grind, Lean's SMT-inspired tactic that combines E-matching, congruence closure, and theory solvers. I will demonstrate the new sym => interactive mode, which gives users explicit control over verification condition generation and discharge, and discuss how AI integration is reshaping how we approach verification at scale. |
| 11:00–11:30 | Coffee break | |
| 11:30–12:30 | Son Ho | Co-development of code and proofs for SymCrypt |
| 12:30–14:00 | Lunch break | |
| 14:00–15:00 | 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 | Verifying Cryptographic Applications: Challenges and OpportunitiesAt Cryspen, we are developing Hax, a toolchain for verifying Rust programs using a variety of backend provers. We have used Hax to verify post-quantum cryptographic libraries, and to analyze implementations of protocols like TLS 1.3 and SPQR for both functional and security properties. In this talk, I will identify the unique challenges in verifying this class of applications, and I will describe how we use tools like F*, ProVerif, and Lean to verify real-world security-critical software. |
Organizing Committee
Ashley Blacquiere (Lean FRO) ✉Oliver Butterley (BAIF) ✉Alessandro D'Angelo (BAIF) ✉Aymeric Fromherz (INRIA)
Venue
Organized by
Partners