English

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

Programming Languages 2019-09-20 v1
Authors: Bruno Bernardo , Raphaël Cauderlier , Zhenlei Hu , Basile Pesin , Julien Tesson
View on arXiv ↗ PDF ↗

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.

Cite

@article{arxiv.1909.08671,
  title  = {Mi-Cho-Coq, a framework for certifying Tezos Smart Contracts},
  author = {Bruno Bernardo and Raphaël Cauderlier and Zhenlei Hu and Basile Pesin and Julien Tesson},
  journal= {arXiv preprint arXiv:1909.08671},
  year   = {2019}
}

Related papers

View all related →
Programming Languages · Computer Science
Making Tezos smart contracts more reliable with Coq
Bruno Bernardo, Raphaël Cauderlier, Guillaume Claret, Arvid Jakobsson +2
2021-06-25
Programming Languages · Computer Science
Albert, an intermediate smart-contract language for the Tezos blockchain
Bruno Bernardo, Raphaël Cauderlier, Basile Pesin, Julien Tesson
2020-01-09
Distributed, Parallel, and Cluster Computing · Computer Science
Introduction to the Tezos Blockchain
Victor Allombert, Mathias Bourgoin, Julien Tesson
2019-09-19
Programming Languages · Computer Science
WhylSon: Proving your Michelson Smart Contracts in Why3
Luís Pedro Arrojado da Horta, João Santos Reis, Mário Pereira, Simão Melo de Sousa
2020-06-01
Programming Languages · Computer Science
HELMHOLTZ: A Verifier for Tezos Smart Contracts Based on Refinement Types
Yuki Nishida, Hiromasa Saito, Ran Chen, Akira Kawata +3
2021-09-13
Logic in Computer Science · Computer Science
Smart Contract Interactions in Coq
Jakob Botsch Nielsen, Bas Spitters
2020-02-10
Programming Languages · Computer Science
Extracting Smart Contracts Tested and Verified in Coq
Danil Annenkov, Mikkel Milo, Jakob Botsch Nielsen, Bas Spitters
2021-04-27
Logic in Computer Science · Computer Science
Finding smart contract vulnerabilities with ConCert's property-based testing framework
Mikkel Milo, Eske Hoy Nielsen, Danil Annenkov, Bas Spitters
2022-10-07
Cryptography and Security · Computer Science
Abstract interpretation of Michelson smart-contracts
Guillaume Bau, Antoine Miné, Vincent Botbol, Mehdi Bouaziz
2022-10-12
Programming Languages · Computer Science
ConCert: A Smart Contract Certification Framework in Coq
Danil Annenkov, Jakob Botsch Nielsen, Bas Spitters
2020-02-05
Logic in Computer Science · Computer Science
Money grows on (proof-)trees: the formal FA1.2 ledger standard
Murdoch Gabbay, Arvid Jakobsson, Kristina Sojakova
2021-12-02
Programming Languages · Computer Science
Translation Certification for Smart Contracts
Jacco O. G. Krijnen, Manuel M. T. Chakravarty, Gabriele Keller, Wouter Swierstra
2022-02-23
Programming Languages · Computer Science
SciviK: A Versatile Framework for Specifying and Verifying Smart Contracts
Shaokai Lin, Xinyuan Sun, Jianan Yao, Ronghui Gu
2021-03-04
Logic in Computer Science · Computer Science
Debugging Smart Contract's Business Logic Using Symbolic Model-Checking
Evgeniy Shishkin
2018-12-04
Programming Languages · Computer Science
Developing secure Bitcoin contracts with BitML
Nicola Atzei, Massimo Bartoletti, Stefano Lande, Nobuko Yoshida +1
2019-08-06
Distributed, Parallel, and Cluster Computing · Computer Science
OV: Validity-based Optimistic Smart Contracts
Quan Nguyen, Andre Cronje, Michael Kong
2020-04-10
Software Engineering · Computer Science
SIF: A Framework for Solidity Code Instrumentation and Analysis
Chao Peng, Sefa Akca, Ajitha Rajan
2019-08-16
Software Engineering · Computer Science
Smart Contracts Formal Verification: A Systematic Literature Review
Rene Davila, Everardo Barcenas, Rocio Aldeco-Perez
2025-10-22
Software Engineering · Computer Science
EOSFuzzer: Fuzzing EOSIO Smart Contracts for Vulnerability Detection
Yuhe Huang, Bo Jiang, W. K. Chan
2020-08-07
Programming Languages · Computer Science
Scilla: a Smart Contract Intermediate-Level LAnguage
Ilya Sergey, Amrit Kumar, Aquinas Hobor
2018-01-03
Logic in Computer Science · Computer Science
Formalising Decentralised Exchanges in Coq
Eske Hoy Nielsen, Danil Annenkov, Bas Spitters
2022-03-16
Software Engineering · Computer Science
A Survey of Smart Contract Formal Specification and Verification
Palina Tolmach, Yi Li, Shang-Wei Lin, Yang Liu +1
2021-04-20
Software Engineering · Computer Science
Validation Framework for E-Contract and Smart Contract
Sangharatna Godboley, P. Radha Krishna, Sunkara Sri Harika, Pooja Varnam
2025-04-29
Logic in Computer Science · Computer Science
Towards benchmarking of Solidity verification tools
Massimo Bartoletti, Fabio Fioravanti, Giulia Matricardi, Roberto Pettinau +1
2024-02-19
Signal Processing · Electrical Eng. & Systems
Keeping Them Honest: a Trustless Multi-Agent Algorithm to Validate Transactions Cleared on Blockchain using Physical Sensors
Nikhil Ravi, Shammya Saha, Anna Scaglione, Nathan G. Johnson
2019-10-25
R2 v1 2026-06-23T11:19:38.600Z