Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts
Bruno Bernardo, Rapha\"el Cauderlier, Zhenlei Hu, Basile Pesin and, Julien Tesson
TL;DR
Mi-Cho-Coq is a Coq-based framework designed to formally verify the correctness of Michelson smart contracts on the Tezos blockchain, enhancing trustworthiness through rigorous certification.
Contribution
It introduces a novel formal verification framework for Michelson smart contracts using Coq, demonstrated through a multisig contract case study.
Findings
Successfully verified a multisig contract using Mi-Cho-Coq
Demonstrated the framework's applicability to real-world contracts
Enhanced confidence in smart contract correctness
Abstract
Tezos is a blockchain launched in June 2018. It is written in OCaml and supports smart contracts. Its smart contract language is called Michelson and it has been designed with formal verification in mind. In this article, we present Mi-Cho-Coq, a Coq framework for verifying the functional correctness of Michelson smart contracts. As a case study, we detail the certification of a Multisig contract with the Mi-Cho-Coq framework.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.