Formal Verification Framework for Michelson

by 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 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 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 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: where we have for all natural numbers (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!

Coinmonks

Coinmonks is a non-profit Crypto educational publication.

Sign up for Coinmonks

By Coinmonks

A newsletter that brings you week's best crypto and blockchain stories and trending news directly in your inbox, by CoinCodeCap.com Take a look.

By signing up, you will create a Medium account if you don’t already have one. Review our Privacy Policy for more information about our privacy practices.

Check your inbox
Medium sent you an email at to complete your subscription.

Coinmonks

Coinmonks is a non-profit Crypto educational publication. Follow us on Twitter @coinmonks Our other project — https://coincodecap.com

Runtime Verification

Written by

Runtime Verification Inc. is a technology startup providing cutting edge formal verification tools and services for aerospace, automotive, and the blockchain.

Coinmonks

Coinmonks is a non-profit Crypto educational publication. Follow us on Twitter @coinmonks Our other project — https://coincodecap.com

Medium is an open platform where 170 million readers come to find insightful and dynamic thinking. Here, expert and undiscovered voices alike dive into the heart of any topic and bring new ideas to the surface. Learn more

Follow the writers, publications, and topics that matter to you, and you’ll see them on your homepage and in your inbox. Explore

If you have a story to tell, knowledge to share, or a perspective to offer — welcome home. It’s easy and free to post your thinking on any topic. Write on Medium

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store