Mi-Cho-Coq，Tezos智能合约认证框架
Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts
摘要：
Tezos是2018年6月推出的区块链。它是用OCaml编写的，支持智能合约。它的智能合约语言被称为Michelson，它的设计考虑到了形式化验证。在本文中，我们介绍了Mi-Cho-Coq，这是一个用于验证Michelson智能合约功能正确性的Coq框架。作为一个案例研究，我们详细介绍了一个Multisig合同与Mi-Cho-Coq框架的认证。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
