# π Start

In this part of the website, we will learn about applying modern **formal verification** to build **software without bugsΒ π**.

Formal verification is proving that a program is correct for **any possible parameters** and initial state, even if there are **infinite possibilities**. The trick for this seemingly impossible challenge is to use **mathematical logic** to reason about the code.

With formal verification, we will see how to build software for which users **can never complain about a bug** and attackers, even with state-level capabilities, **can never exploit a vulnerability**. Formal verification has been used successfully for critical systems such as **rockets going to spaceΒ π§βπ**, trains, airplanes, and more recently to **securing cryptocurrenciesΒ π°**.

For the learning, we will follow the adventures of **JejuΒ π»ββοΈ**, a small bear lost on an island who is very keen on never making mistakes.

## Formal verificationβ

There are rules to follow to reason about the code in a logical way. These rules apply to each primitive instruction in a programming language, such as `if`

, `while`

, `for`

, `return`

, etc. There is also a way to specify the expected behavior of a program, to distinguish between a **bug** and a **feature**. Distinguishing between a bug and a feature might be one of the hardest things to do, as there is not a single answer fitting every situation. Stating what a program should do is called a **specification**.

Jeju the bear π»ββοΈ knows the ancient art of formal verification. He is fortunate to use the **CoqΒ π** proof software that helps write down all the reasoning **without making mistakes**. The Coq system has now been existing for 40 years and continues to evolve. It uses a special kind of logic based on dependent types, in which we can express any **mathematical statement** or **property about a program** and verify it. Many other systems are also based on these ideas, such as Lean or Agda.

## Quick exampleβ

We now look at a small example to see the difference between testing and formal verification. You do not need to understand all the details for now.

To find bugs in a program the traditional method is to test many parameters until we can see the program working fine enough times. However there can always be a missing bug on a case that we have not tested. Here we take a small example to show the difference between testing and formal verification.

### Rust programβ

This is a Rust program returning the opposite of an integer:

`fn opposite_i8(n: i8) -> i8 {`

return -n;

}

The type `i8`

represents signed integers in 8 bits. If we test this function, it will work for most cases:

`fn main() {`

println!("{}", opposite_i8(0)); // prints 0

println!("{}", opposite_i8(40)); // prints -40

println!("{}", opposite_i8(-28)); // prints 28

}

But there is one case in which the function fails:

`// You need to run this code in release mode as in debug mode`

// the overflows are checked and the program instead panics

fn main() {

println!("{}", opposite_i8(-128)); // prints -128 instead of 128

}

The reason is that the bounds of 8 bits integers are from `-128`

to `127`

so we cannot represent `128`

and thus we get a wrong result, in this case `-128`

.

### Coq versionβ

To be extra safe, Jeju uses formal verification and even sometimes avoids writing any tests!

Here is how he would represent the above program in Coq. We do not have an `i8`

type but we have the `Z`

type of integers without bounds. We simulate `i8`

numbers by a function that takes an arbitrary integer and puts it back into the `-128`

and `+127`

bounds using the modulo operator:

`Definition normalize_i8 (n : Z) : Z :=`

((n + 128) mod 256) - 128.

We then define the opposite function:

`Definition opposite_i8 (n : Z) : Z :=`

normalize_i8 (-n).

that returns the same results as in Rust:

`Compute opposite_i8 0. (* 0 *)`

Compute opposite_i8 40. (* -40 *)

Compute opposite_i8 (-28). (* 28 *)

Compute opposite_i8 (-128). (* -128 *)

### Formal verificationβ

We can now state that the `opposite_i8`

function should work for all `i8`

values except `-128`

:

`Lemma normalize_i8_eq (n : Z) :`

- 127 <= n <= 127 ->

opposite_i8 n = - n.

It says that for all integers between `-127`

and `127`

the opposite function returns the same value as what we would have in `Z`

. We need to write an argument to say that this property is always true as the Coq system cannot check everything by itself. The argument is called a proof and is the following:

`Proof.`

unfold opposite_i8, normalize_i8.

lia.

Qed.

It says that we unfold all the definitions and then run the linear arithmetic solver `lia`

to conclude the proof automatically. Once someone knows about the Coq proof system this is a very natural proof to write. For the proof above to work, you need to activate the division mode for `lia`

with:

`Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.`

If we use an interval starting at `-128`

instead, the same proof fails as expected:

`Lemma normalize_i8_eq (n : Z) :`

- 128 <= n <= 127 ->

opposite_i8 n = - n.

Proof.

unfold opposite_i8, normalize_i8.

lia.

Qed.

returns the error:

`Error: Tactic failure: Cannot find witness.`

### Conclusionβ

We have seen how to both test and formally verify a small program `opposite_i8`

. As there are only `256`

possible values between `-128`

and `127`

, we could have also tested it exhaustively. But if we were working with the `i64`

type instead, for signed integers with 64 bits, there would be too many possible values to test. That does not make Jeju afraid as the proof for 64-bits integers takes about the same time to run, a fraction of a second, and confirms that `opposite_i64`

is valid for all `i64`

values except the minimal one! π

## Nextβ

The rest of the learning section is under construction. We will learn:

- The basics of the Coq system.
- How to write a specification for a program in Coq and verify it?
- How to use Coq to verify smart contracts in Solidity?
- How to use Coq to verify Rust programs?

J. πΎ