May 21
Loading video player...
Anja Petković Komel: From smart contracts to proof assistants – the act verification framework for Ethereum smart contracts May 14, 2026 Seminar for Foundations of Mathematics and Theoretical Computer Science Faculty of Mathematics and Physics University of Ljubljana Abstract: What happens when you put millions of dollars in a computer program that no one can stop or modify? You get Ethereum smart contracts — and a compelling case study for formal verification in the wild. Proof assistants are no longer confined to the ivory tower: they are increasingly applied to real-world critical software. In this talk, I will present act, a formal verification framework for Ethereum smart contracts via SMT solvers. At its core, act is a typed intermediate specification language with mechanised meta-theory (type safety, proved in Rocq). It sits between and is connected to source languages (like Solidity and Vyper) and proof assistants (Lean and Rocq). We will look briefly at how smart contracts work, then build an act specification for a concrete contract: automatically verifying its equivalence to a Solidity implementation, and stating and proving correctness properties interactively in Lean, leveraging the representation of smart contracts as a state transition system. This is joint work with Zoe Paraskevopoulou, Lefteris Lazaropoulos, Sophie Rain and Alexis Terry.