Advanced Topics
Introduction
Last Updated: 30th June 2023
One of the great benefits of Tezos is the ability to formally verify smart contracts. Tezos makes this formal verification possible for smart contracts with the design of Michelson and with tools such as Coq and the Mi-Cho-Coq library.
This entire section walks through formal verification and how it relates to Tezos:
Formal Verification on Tezos discusses how smart contracts on Tezos can be formally verified, its benefits, and what tooling makes this possible.
Modelling for Smart Contracts goes through an example smart contract, its formal specification and its proof.
Coq gives a brief introduction to syntax and proof creating on Tezos using Mi-Cho-Coq.
Mi-Cho-Coq discusses what Mi-Cho-Coq is and how it bridges between Tezos smart contracts and formal proofs in Coq.
Visual Overview
The image below helps visualise the process for performing formal verification for Tezos smart contracts:
Further Reading
For mathematicians and very curious developers, an extra theoretical section will introduce some basic concepts of Type theory such as GADT which allows inductive types on the Calculus of Inductive Construction (CiC). The proof assistant Coq, which is based on the CiC, can be used for proving theorems.