Introduction
The Tezos blockchain has several advantages over its concurrents. 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.
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).