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.
Cite
@article{arxiv.2106.12973,
title = {Making Tezos smart contracts more reliable with Coq},
author = {Bruno Bernardo and Raphaël Cauderlier and Guillaume Claret and Arvid Jakobsson and Basile Pesin and Julien Tesson},
journal= {arXiv preprint arXiv:2106.12973},
year = {2021}
}