Julian leads the formal verification team at Nethermind, developing hard formal methods-based solutions to formally verifying the web3 ecosystem. Previously he completed his PhD at Imperial College on "Compositional termination verification for fine-grained concurrency" using separation logic.

Julian Sutherland

Join us for an in-depth workshop on the Clear framework, a cutting-edge tool designed for the formal verification of smart contracts by extracting Yul code into Lean. This workshop will explore Clear’s remarkable expressivity, enabling any pen-and-paper proof of correctness to be mechanized in Lean. Participants will learn about Clear's compositionality and abstraction, allowing scalable verification of complex smart-contracts, and its automation capabilities to streamline proof generation.

Classroom A

Clear: a Formal Verification framework for smart contracts in Lean

Vitalik believes "ethereum's biggest technical risk probably is bugs in code, and anything that could significantly change the game on that would be amazing".  Formal verification is a key technology which many believe could significantly help.  However, it has yet to see wide adoption for a variety of reasons.  This panel will bring together formal verification experts working in blockchain to discuss the challenges faced in increasing the use of formal verification within the community.

I’m a research engineer in the Automated Reasoning Team at ConsenSys. My current focus is on the practical application of formal methods to software correctness, such as for zkEVMs. Previously, I was an Associate Professor at Victoria University of Wellington, NZ. My research interests are in programming languages, compilers, static analysis and formal verification

David Pearce

Igor Konnov is an independent security & formal methods researcher, working on the project "Exploring Automatic Model-Checking of the Ethereum specification" supported by Ethereum Foundation. He has experience of integrating formal methods in the blockchain development process since 2019. Igor was the principal investigator in the projects Quint and Apalache. Before joining the blockchain industry, he worked as a formal methods researcher at Inria Nancy, TU Wien, and Lomonosov Moscow State Univ.