# 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.

FIGURE 5: Overview of the formal verification process on 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).