Formal verification is the act of proving or disproving that a program, like a smart contract, respects its formal specification, using formal methods of mathematics.

A formal specification uses a formal language to describe *what* the program is supposed to do. A formal language is defined by a grammar (a set of rules that define how sentences are formed). Programming languages are also formal languages, but they say something about *how* the program does what it does.

The formal aspect of the specification makes it possible to automatically analyze whether the program verifies it or not. A fundamental result of computer science is that it is *not* possible to decide automatically whether any program verifies any specification.

The verification process is thus a mixture of automatic and manual *formal* proving steps.

## #

BenefitConsider the following program:

`function sum(n : int) = if n > 0 then n + sum(n - 1) else 0`

And the formal specification *P*:

`forall n, n >= 0 -> sum(n) = n * (n + 1) / 2`

which reads: for every integer n, if n is above 0, then `sum(n)`

is equal to n multiplied by n plus 1, divided by 2.

How to make sure that `sum`

verifies *P*?

You can either write a test program that computes the `sum`

function for a large range of values, say for `n`

from 0 to 1000000, and checks the formula; or you can *mathematically* prove the property (with inductive reasoning for example) in a few reasoning steps.

While you may be reasonably confident in the test program, and by transtion in the `sum`

function, the property is only tested on a limited set of values, and the test program may itself contain bugs. The question to decide whether the test is correct is stil not decidable on a systemic level.

With mathematic reasoning, properties are proven for any parameter value, and the confidence in the proof relies on whether it is correct or not.

Another fundamental result is that it *is* possible to automatically decide whether a proof is correct or not, as long as it is formalized. Hence the confidence you get with formal methods does not rely on the confidence you may give the developper of the program and tests, but it relies on the *existence* of a correct formal proof.

As such, formal verification provides *trust-less* confidence. That's why it is a key point for the development of smart contracts bacuse, with smart contracts, blockchains had lost their trust-less execution feature; they claim it back with formal verification.

## #

LimitsFormal verification is relative to the specification. It is possible that a verified program does not behave as expected if this expectation has not been formalized in the specification.

Another caveat of formal verification is the difficulty to read specification. What confidence can you have in a verified program if you do not understand its specification?

At least, the trust in the verification relies on the trust in the tools used to build and check the proof. The set of tools that the process relies on is called the Trusted Computing Base.

That's why it is suggested to *complement* the verification approach with standard tests, especially to cover specification areas that are harder to formalize or verify.

## #

ProcessThe formal verification process is two steps:

- write the formal specification of the contract
- prove the contract verifies the specification with formal method systems

Writing formal specification is a key step of the verification process because it defines the perimeter of the verification. This task requires knowing the technical and business context of the contract execution, in order to describe accurately the contract's behavior.

It also requires knowing a formal specification language, which is equivalent to knowing a programming language. While there is no systemic method to write formal specification, it may follow some basic principles, presented in this guide.

Proving that the contract verifies the specification is a technical task that requires training and skills in formal logic and formal method tools.