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.