Making Tezos smart contracts more reliable with Coq

TL;DR

This paper presents a framework using the Coq proof assistant to formally verify Michelson smart contracts on the Tezos blockchain, enhancing their reliability and correctness.

Contribution

It introduces Mi-Cho-Coq, a Coq library for formal semantics and reasoning about Michelson, and Albert, an intermediate language with a Coq-implemented compiler.

Findings

Developed Mi-Cho-Coq for formal verification of Michelson contracts

Created Albert, an intermediate language with a Coq-based compiler

Enabled formal reasoning and verification of smart contract correctness

Abstract

Tezos is a smart-contract blockchain. Tezos smart contracts are written in a low-level stack-based language called Michelson. This article gives an overview of efforts using the Coq proof assistant to have stronger guarantees on Michelson smart contracts: the Mi-Cho-Coq framework, a Coq library defining formal semantics of Michelson, as well as an interpreter, a simple optimiser and a weakest-precondition calculus to reason about Michelson smart contracts; Albert, an intermediate language that abstracts Michelson stacks with a compiler written in Coq that targets Mi-Cho-Coq.