Formal Verification Framework for Michelsonby Stephen Skeirik
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.
This is where RV enters the picture. Over the past decade, RV has developed the K framework, a toolkit for designing programming languages and automatically generating interpreters, static analysis tools, model checkers, and theorem provers. Using this toolkit, RV gained significant experience specifying, formalizing, and verifying blockchain protocols, languages, and programs. As part of two previous grants from the Tezos Foundation, we formalized the Michelson language in our K-Michelson interpreter as well as created a Michelson unit testing framework. In this grant, we will extend our existing unit testing framework for Michelson to enable formal verification of Michelson smart contracts!
For those unfamiliar with formal verification, the idea is simple: it is a technique to mathematically prove that a program is correct. Due to its mathematical nature, it provides us with the strongest possible guarantees of program correctness. Traditional software testing approaches can only prove the presence of failure in the sense that, even if our tests pass, our software still may have bugs. On the...