Title: Multi-Modal Verification of Distributed Systems in Lean

Speaker: Ilya Sergey   (bio) (bio)

Ilya Sergey is an Associate Professor at the School of Computing of National University of Singapore, where he leads the Verified Systems Engineering lab. He received his PhD from KU Leuven. Before joining NUS, he was a postdoc at IMDEA Software Institute and a faculty at University College London. Ilya's research spans programming language design, software verification, and distributed systems. He is a Program Committee Co-Chair for OOPSLA'27, was General Chair for ICFP 2025, and organised the ICFP Programming Contest in 2019. He is the recipient of several POPL/PLDI distinguished paper awards, the 2019 Dahl-Nygaard Junior Prize, and research awards from Google, Meta, and Amazon.

When: Tuesday, 14 July 2026 at 1930 hrs (IST)  

Meeting Details: Zoom link, ID: 891 6409 4870, Passcode: 082194

Abstract:
In this talk, I will present Veil, a framework for automated and interactive verification of transition systems, aimed specifically at conducting machine-assisted proofs about concurrent and distributed algorithms. Veil is implemented on top of the Lean proof assistant. It allows one to describe a transition system and its specification in a simple imperative language, verifying it using both dynamic and symbolic execution techniques.

Veil allows one to check the desired safety properties in the style of TLA+ using explicit-state model-checking. For symbolic deductive reasoning, Veil produces verification conditions in first-order logic, to be discharged automatically via a range of SMT solvers. In case automated verification fails or if the system's description requires statements in a higher-order logic, Veil provides an interactive verification mode, by virtue of being embedded in a general-purpose proof assistant. Veil's automated verification performance is acceptable for practical verification tasks, while it also allows for seamless automated/interactive verification of system specifications beyond the reach of existing automated provers.