How model checking can help build trust in the design of distributed protocols like Single Slot Finality
Duration: 00:06:19
Speaker: Igor Konnov, Thanh-Hai Tran
Type: Lightning Talk
Expertise: Intermediate
Event: Devcon
Date: Nov 2024
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
