11-13, 11:20–12:50 (Asia/Bangkok), Classroom A
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.
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.