Veil: A Framework for Automated and Interactive Verification of Transition Systems
15/8/2025, 3:00pm
Speaker
Abstract
We present Veil, an open-source 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, producing 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. We have evaluated Veil on a large set of case studies from the distributed system verification literature, showing that its 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. This work was publicised by the department as a Research Highlight on August 4th.
Bio
George Pîrlea is a fifth-year Ph.D. candidate at the National University of Singapore, supervised by Ilya Sergey. His research interests include Lean, formal methods, programming languages, distributed systems, and cryptography.