Nomadic Labs knowledge center

Searchβ¦

Understanding the Tezos blockchain

How-To

Decentralized Applications

β

Formal Verification

Introduction

The Tezos blockchain was designed to ensure the required security and compliance of the code, particularly for high-value use cases such as the issue and management of *Security Tokens** **ΒΉ*, *stablecoins* **Β²**, or even for the freezing of funds in a context such as *liquidity pools* **Β³**.

Any contract deployed on a public blockchain is almost impossible to rewrite or remove from the chain history. Consequently, for certain applications, unit tests are insufficient for ensuring that they have the desired operation. It is therefore essential to prove the correct operation of these contracts via formal verification.

In this document, we shall explain what formal verification of smart contracts is and illustrate it with Mi-Cho-Coq, the formal verification tool developed by Nomadic Labs.

From that point, it may no longer transfer its funds. Nevertheless, it receives LP tokens, which represent its part of the pool. It may, when it decides to do so, recover its funds. It also receives the exchange fees paid by the service users.

Definition of the main concepts

β**Coq****:** Formal proof assistant that provides a formal language for writing mathematical definitions, executable algorithms, and theorems with a semi-interactive environment for developing proof verification. A prominent tool that is well established in code verification, particularly in critical areas.

Motivations

During the design of smart contracts, it is important to ensure that they are doing what they were designed to do.

Owing to the data that they handle and because, once deployed, you can no longer simply change the code, it is necessary to have guarantees for the security of the code: in other words, that its execution behaves as predicted by the specifications.

In fact, in certain areas where there is a low margin for error, a code that reacts unpredictably may be very costly and incur heavy human and financial consequences.

Ensuring that a smart contract is behaving correctly is not a trivial task. A standardized good practice is to carry out unit tests. In reality, such tests only cover a finite number of cases. Consequently, how do we ensure that a program matches its specification and is mathematically correct?

This is where formal verification comes in. All methods and tools that address this issue constitute formal methods. It involves methods based on a mathematical representation of a program that allows reasoning about it. They are ranked according to the level of guarantees that they provide: from bug detection (tests, PBT testing, model-checking, etc.) to code correction and even the generation of correct code by construction.

The idea then is to find a mean of **translating these smart contracts** into a language **that will be used in a proof assistant** (this is where Coq comes in). Before their deployment, certain smart contracts may be considered critical, requiring a detailed audit. In this case, in addition to unit tests, they can be formally proven, using the Coq proof assistant.

It should be noted that there are other tools for verifying smart contracts on the Tezos blockchain. The main ones include:

- βK-Michelson: Michelson interpreter developed by Runtime Verification, which develops a generic language specification tool, K-framework.

Some syntactical elements of the Coq language

Coq language:

- Boolean type definition:

```
Inductive bool : Type :=
| true
| false.
```

- Definition of a function that returns the denial of a Boolean:

```
Definition negb (b:bool) : bool :=
match b with
| true => false
| false => true
end.
```

A few syntactical elements of the Coq language

Here is an example of proof that may be implemented:

```
Example test_orb1: (orb true false) = true.
Proof.
simpl. (* ===> true = true *)
reflexivity. (* ===> no more subgoals *)
Qed.β΄
```

In the example above, it involves showing that *true or false *equals* true*. The first line matches the one that we want to demonstrate. The lines between the *Proof* and *Qed* keywords constitute the proof.

All words between Proof and Qed are called **tactics**. These are functions that allow us to make our demonstration step by step.

All tactics are referenced at: https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacv.destruct-eqnβ

Proof creation using Mi-Cho-Coq

As Coq is a proof software that has its own syntax; the difficulty has been in finding a way to translate the Michelson code into Coq.

Mi-Cho-Coq is the library that allows you to do this. When you wish to prove a smart contract written or compiled down in Michelson, you must use this library and import the code that you wish to formally prove. The syntax to be used at the start of the file containing the proof is as follows:

```
Require Import Michocoq.macros. Import syntax.
Require Import Michocoq.semantics. Require Import Michocoq.util.
Import error.
```

For a more technical understanding of the operation of Mi-Cho-Coq, this tutorial can be viewed: https://βgitlab.com/nomadic-labs/mi-cho-coq/β

Execution of a simple proof using Coq software

We shall execute the proof of: **Example test_orb2** (Example keyword below) using the Coq proof assistant.

Proof execution with the Coq software 1/3

Proof execution with the Coq software 2/3

Proof execution with the Coq software 3/3

End of proof.

Limitations

Here are the main limitations of formal logic:

Limitation of a general nature:

- It is
**difficult to formally define the expected behavior of a contract**, and a proof depends on the quality of the formal definitions associated with it. Consequently, a poorly defined contract may, even if it has been formally proven, have undesirable behaviors.

Limitations specific to Mi-Cho-Coq:

- A formal proof of a smart contract
**does not evaluate possible problems related to its Gas consumption**(Unit of measurement of the cost of executing a smart contract in time and computer resources. A price in tez will correspond to a quantity of Gas.). Consequently, a dedicated assessment to evaluate the cost of a smart contract is relevant to complement the formal logic proofs. - Mi-Cho-Coq allows you to show a contractβs calls but
**not on a series of several independent calls**. However, other tools allow you to do this; this is, for example, the case of Concert (Certification tool for smart contracts in Coq.).

Conclusion

Mi-Cho-Coq is a tool that allows you to obtain certain guarantees with regard to the execution of a smart contract deployed on the Tezos blockchain. In fact, when it involves creating and deploying smart contracts, it is essential to verify that the code meets the specification that characterizes it.

Nowadays, many smart contracts deployed with prior audit and unit tests have shown serious flaws, particularly in the context of *DeFi** ***β΅**, which increases the risks of financial losses if a flaw is detected. During the creation of smart contracts, in addition to unit tests, formally verifying the program created, using a proof software helps to reduce considerably the possibility of vulnerabilities and undesirable behaviors of the code.

The Tezos blockchain and its code were designed and developed in order to obtain a high level of code security guarantees, either through technological choices or its architecture. In particular, its native Michelson smart contract language facilitates formal verification. This is why it is generally easier to formally prove contracts on the Tezos blockchain, compared to other blockchains whose smart contract languages do not facilitate formal verification.

Mi-Cho-Coq has, in particular, helped to formally verify the standard of FA1.2 tokens on Tezos, Dexter 2 (version 2 of the decentralized Dexter exchange platform), Liquidity Baking (a single-asset decentralized exchange offered by the Granada amendment), or even the multisignature contract used by the Tezos client.
**[5]:** Decentralized Finance - All financial applications based on smart contracts. Some of these application cases are similar to so-called traditional finance such as loans.