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.

翻译：Tezos是一个智能合同链。Tezos智能合同是用一种叫做Michelson的低级堆叠语言撰写的。文章概述了利用Coq验证助理对Michelson智能合同给予更有力保障的努力:Mi-Cho-Coq框架,一个Coq图书馆,界定Michelson的正式语义,以及一名口译员、一个简单的美食师和一个最弱的预设微分数,以解释Michelson智能合同;Albert,一种中间语言,即Michelson与一个以Mi-Cho-Coq为对象的Coq编译者拼凑在一起。