What is formal verification, and why is it important for smart contracts?

Question

"Formal verification" has appeared in various previous questions and answers, and I believe was the topic for one of the talks at DevCon2.

Main question: It's perhaps quite broad, but what is formal verification in the context of Ethereum, and why do we need it for smart contracts?

Sub-questions:

1. Is it something that's already implemented and part of the ecosystem, or is it something that will be implemented in future?
2. How is formal verification different to the inherent determinism of the language a smart contract is written in? (See Why do smart contract languages need to be deterministic?)

Answer 1

Main question. Formal verification is a method to prove a program correct for all inputs. It involves proving (unless the state space is small enough for model checkers). After somebody proves a property of a smart contract, even malicious attackers cannot find any input that breaks the proven property of the contract (unless the real EVM does something different from the EVM used in verification).

Sub-question 1. The good news is that EVM has been defined for interactive theorem provers. Some small example contracts have been verified. Formal verification is not in the ecosystem yet. (The Solidity-to-Why3 translation should not be trusted because it is not even tested.) I think the quickest way forward is to develop a smart contract language within an interactive theorem prover.

Sub-question 2. Formal verification is a human activity while the inherent determinism of the language is a property of the language.

Answer 2

Formal verification means applying a proof that the program behaves according to a specification. In general, this is done with a concrete specification language used to describe how input and output of functions should relate.

So why is it important for smart contracts? You could imagine: (1) smart contracts are immutable, you can't patch them easily, (2) smart contracts store value and are (3) accessible publicly from all over the world. This makes them very attractive for hacker attacks. Formal Verification is a strong approach to reduce the risk of bugs and attacks.

Formal verification can be quite sophisticated with mathematical models describing the problem, but also very simple. Some consider Unit Testing the simplest form of formal verification. The trick is always to describe the behavior of an algorithm without reproducing it, having an outside look.

Subquestion 1: Browsersolidity already supports it to a small extend using the formal verification language why3.

Subquestion 2: this should be clear now, they don't depend on each other, but: deterministic algorithms are much easier to prove than non-deterministic, therefore formal verification is a good idea for Ethereum

Answer 3

Formal Verification is needed for the same reason its needed in any other language or application, because Unit Testing cannot test each permutation or condition.

You might test boundary conditions in requirements-based tests and achieve full code-coverage and infer this means you are secure because you have tested and exercised every line of code. Formal Verification if done right can prove that all intermediate permutations are tested too.

The hardest part of Formal Verification is mathematically representing the inputs and context in which they are used. For that reason even with Formal Verification, security features such as pauseable contracts should be considered.