Formal Specification and Verification of the Distributed Validator Technology protocol

Visit the https://archive.devcon.org/ to gain access to the entire library of Devcon talks with the ease of filtering, playlists, personalized suggestions, decentralized access on IPFS and more. https://archive.devcon.org/archive/watch/6/formal-specification-and-verification-of-the-distributed-validator-technology-protocol/index In this talk, we present our work on formally specifying and verifying the Distributed Validator Technology (DVT) protocol, using the verification-ready programming language Dafny, to ensure that the DVT protocol behaves as expected. You will learn how to read the formal specification, how to use it to write your own implementation of the protocol, what properties we have formally proven to be guaranteed by the protocol and what the future directions of the DVT protocol and our work are. Speaker(s): Roberto Saltini Skill level: Intermediate Track: Staking & Validator Experience Keywords: Distributed Validator Technology,formal verification,Dafny Follow us: https://twitter.com/efdevcon, https://twitter.com/ethereum Learn more about devcon: https://www.devcon.org/ Learn more about ethereum: https://ethereum.org/ Devcon is the Ethereum conference for developers, researchers, thinkers, and makers. Devcon 6 was held in Bogotá, Colombia on Oct 11 - 14, 2022. Devcon is organized and presented by the Ethereum Foundation, with the support of our sponsors. To find out more, please visit https://ethereum.foundation/