Introduction
Tezos has several advantages over other blockchain. One of them is the formal verification of smart contract. This module shows a brief overview of how Tezos smart contracts can be formally verified.
We will first define in the Generalities section what is the formal verification of a Tezos smart contract, and its benefits and how proof assistants (and tools) can make this task possible.
An explained example (Vote smart contract) will be used to illustrate the formal specification of a Tezos smart contract, and its proof.
The schema below describes the process for performing formal verification on Tezos smart contract.
For mathematicians and very curious developers, an extra theoretical section will introduce some basic concepts of the 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.
This extra theoretical section will also introduce Coq and the Mi-Cho-Coq library (used by Coq) to formalize a smart contract as a logical object (theorem). This theorem is formalized in Gallina (Term) language, which follows the CiC principles. The script for proving the theorem is written in Gallina (Vernacular), which provides tactics and will be executed by the inference engine (Coq).