  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.
