11-15, 10:30–10:40 (Asia/Bangkok), Stage 4
Ethereum is a lively place for developing distributed protocols. Getting a distributed protocol right is a notoriously difficult task. When it comes to developing the Ethereum CL, the community follows two pragmatic approaches: Writing pen & paper proofs and writing executable specs in Python. We show how model checking can confirm our intuition about the behavior of consensus protocols or disprove it. We do so by applying our method to one of the recently proposed Single Slot Finality protocols
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.
Thanh-Hai Tran is an independent researcher. Before that, he was a senior researcher in the Dependable Distributed System team at Consensys. His interests are formal methods, distributed systems, cryptography, and blockchains. He has experience in designing blockchain protocols, applying formal verification techniques in multiple projects, e.g., the Distributed Validator Technology (DVT), the 3-Slot-Finality (3SF) protocol, and the C-KZG library, and developing analysis tools, e.g., APALACHE.