Software verification

Developments

Mi-Cho-Coq

The Mi-Cho-Coq project is a specification of the language of smart-contracts Michelson in the theorem prover Coq. This provides a formal specification of the syntax and semantics of Michelson, as well as a framework to verify smart contracts.

Albert

The language Albert is an intermediate smart contract programming language compiled to Michelson. Albert is an imperative language with variables and records, abstracting the Michelson stack. The intent of Albert is to serve as a compilation target for high-level smart contract programming languages. The linear type system of Albert ensures that an Albert program, compiled to the stack-based Michelson language, properly consumes all stack values.

Publications

Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts

Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, and Julien Tesson

FMBC 2019, October 2019 (pdf)

Tezos is a blockchain launched in June 2018. It is written in OCaml and supports smart contracts. Michelson is the smart-contract language of Tezos and has been designed with formal verification in mind. In this article, we present Mi-Cho-Coq, a Coq library for verifying the functional correctness of Michelson smart contracts. As a study case, we detail the certification of a Multisig contract with the Mi-Cho-Coq framework.

Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts

Bruno Bernardo, Raphaël Cauderlier, Zhenlei Hu, Basile Pesin, and Julien Tesson

The Coq Workshop, September 2019 (pdf)

We present Mi-Cho-Coq, a Coq library for verifying the functional correctness of smart contracts running in the Tezos blockchain.

Albert, an intermediate smart-contract language for the Tezos blockchain

Bruno Bernardo, Raphaël Cauderlier, Basile Pesin, and Julien Tesson

4th Workshop on Trusted Smart Contracts, February 2020 (pdf)

Tezos is a smart-contract blockchain. Tezos smart contracts are written in a low-level stack-based language called Michelson. In this article we present Albert, an intermediate language for Tezos smart contracts which abstracts Michelson stacks as linearly typed records. We also describe its compiler to Michelson, written in Coq, that targets Mi-Cho-Coq, a formal specification of Michelson implemented in Coq.