In a previous post, we introduced the K-Michelson project, a formal verification framework for Michelson smart contracts, and described our overall project goals. In this two-part series, we will investigate:
- What an ideal programming language specification looks like.
- How this ideal framework powers nextgen program testing.
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.
In this second part of our four part series, we will discuss the process of formalizing system requirements and how it fits into the larger context of formal verification for blockchain systems and smart contracts.
Recall that formal verification is all about knowing whether our system implementation (e.g., blockchain system/smart contract), satisfies our system requirements.
Today’s article is about the process of converting our requirements document into an equivalent formal, mathematical requirements specification.
Blockchain technology coupled with smart contracts offers a tantalizing promise: enabling distributed, trusted, and verifiable computational platforms for applications with rigorous security requirements like finance, secure messaging, and more. Unfortunately, one does not have to look very hard to see that the path to this promise is fraught with danger, e.g., see articles on Mt. Gox, the DAO, this attack on Ethereum classic, and a smart contract bug. While blockchain systems may be sound in theory, in practice, blockchain systems and smart contracts are still highly prone to developer error.