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.

FIGURE 5: Overview of the formal verification process on smart contract.For mathematicians and very curious developers, an extra [theoretical](/formal-verification/gadt-coq) 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).