Formal Verification Framework for Michelson

Introduction

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 other hand, formal verification gives us a means to say, once and for all, that our program is bug-free.

Of course, the power of formal verification doesn’t come for free. Traditionally, companies have hired formal verification experts (such as ourselves!) to apply our expert knowledge to solve their verification problems. The purpose of this grant is to create a formal verification framework for the Michelson smart contract language that enables Michelson developers without expert knowledge to formally verify contracts.

An Inside Look

This section is for the curious and technically-minded folk who want to peek under the hood to see how this all works.

Before we co-developed the Michelson unit testing framework with the Tezos Foundation, the Michelson developer needed to write both their contracts, typically using the .tz extension, as well as custom code for running tests using the Tezos client. Now developers can write tests which run locally and deterministically using the .tzt format and the K-Michelson interpreter. Here is an example unit test file:

The test file format states: given an input stack containing just the natural number 5, after executing the code in the code block, check that I obtained an output stack containing just the natural number 5.

For those familiar with the Michelson language, you may realize that this code implements an identity function for the natural numbers, that is, it implements the function: identity(n) where we have identity(n) = n for all natural numbers n (there are much simpler ways to write this function---we use this implementation for demonstration purposes). To gain more confidence that our code is correct, we could write more test cases, replacing the number 5 with 6, 18, or even 19,727. But what if we want to prove that our code implements an identity function. How can we do that?

There are too many details involved to describe in this short blog post. The important point is: by making a few tweaks to our test file, using only Michelson-like notation, we are able to transform our standard unit test into a symbolic unit test which proves, once and for all, that our code implements a bona fide identity function. The updated test file is as follows:

Though we still need to know about a few concepts such as loop invariants, an abstract summary of the behavior of a loop (for the curious, read more about loop invariants here and here), amazingly enough, we can express ourselves confidently and precisely without needing to learn the complex mathematical notation involved in standard program verification approaches.

Conclusion

Bringing on Runtime Verification through the Tezos Ecosystem Grants program signals Runtime Verification and Tezos Foundation’s shared commitment to empowering Michelson smart contract developers to write smart contracts more safely and effectively which, in turn, will help realize our vision of a thriving blockchain ecosystem.

This brief summary and example is just a taste of what is possible. As we continue to work on this grant, we will be adding more features, supporting a larger fragment of the Michelson language, and improving performance as well as the user experience. Stay tuned for more updates or follow along with our progress at our GitHub repository!