We are pleased to announce that Runtime Verification has been awarded a grant by Algorand Foundation to develop a formal semantic framework for Algorand’s smart contracts. The grant is part of its recently launched 250 Million ALGO Ecosystem Grants Program, a multi-year program that aims to support research and development of the Algorand ecosystem. We are very excited to have the opportunity to collaborate with Algorand in forming the future of Algorand’s smart contract architecture and supporting its growing community of developers. We have previously successfully completed a prior engagement with Algorand to formally model and verify safety of the platform’s consensus protocol, and we look forward to using the knowledge and experiences gained in this new engagement.
Runtime Verification Inc. (RV) is pleased to announce that we are partnering with the Tezos Foundation via the Tezos Ecosystem Grants program to develop a formal verification framework for the Michelson smart contract language! From its inception, the Tezos blockchain was designed with convenience, security, and extensibility in mind. However, unlike the status quo of predecessor technologies like Bitcoin, the true vision of a thriving Tezos ecosystem is more than just a secure digital currency exchange―it is a platform for developing and publishing distributed applications via smart contracts using its smart contract language Michelson. To fully realize this vision, Michelson smart contract developers will require tooling that enables them to confidently write and test smart contracts.
Musab A. Alturki, Elaine Li and Daejun Park
Gasper is an abstract proof-of-stake protocol layer that is implemented by the Beacon Chain protocol, the underlying protocol of the upcoming Ethereum 2.0 network. A key component of Gasper is a finality mechanism that ensures durability of transactions and the continuous operation of the system even under attacks.
We are happy to report the successful completion of another major milestone in an ongoing collaboration between Runtime Verification and Ethereum Foundation, to build a formal framework for modeling and verifying the Beacon Chain. We have formally proved key correctness properties of finality in Gasper and used these results to show that these properties also hold in an abstraction of Gasper’s implementation in the Beacon Chain. The models and proof scripts are all available online.
In this post, we focus on the first part of this achievement, which is verifying Gasper’s properties. So what’s Gasper? How are its properties formally verified? And why is this important?