11-13, 09:45–10:45 (Asia/Bangkok), Classroom A
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
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.
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.
