Tools

The Tezos community provides a rich technical and human eco-system regarding formal verification:

ToolsDescription
MichocoqA specification of Michelson in Coq to prove properties about smart contracts in Tezos.
ArchetypeArchetype provides a specification language for contract invariant and entry point postconditions. It generates the contract in the Why3 language for verification
Coq is an interactive proof assistant. The user sends instructions to the proof engine to build up the proof step by step: apply a theorem to justify a proposition, rewrite a term by another and so on. It is possible to program macros for automation purpose. Proving a program in Coq requires the language semantic in Coq theory (provided by Michocoq for Michelson) used to prove the correctness of the program.

Why3 is a plateform dedicated to program verification: it translates the program and specification into SMT problems (called proof obligation) for SMT solvers to solve. When solvers succeed, the verification is automatic. When solvers fail, it is necessary to help them by providing intermediate properties about the program, that they can solve, and that they can use to solve the problem.

Archetype#

The Completium contract templates have been formally specified with Archetype.

Specification language#

The Archetype specification language documentation is available here.

In a nutshell, what can you specify with it?

  • entrypoints' postconditions: a postcondition is a property about what the execution of the entrypoint changes in the contract's storage.
  • entrypoints' fail conditions: a fail condition is a property that holds true when the entrypoint is fails
  • contract invariants: an invariant is a property about the contract's storage that is always true, regardless of the transactions history.

Whyml#

Archetype generates the contract's code and specification in whyml, the Why3 language.

The following Completium CLI command:

completium-cli generate whyml elementary.arl

generates the whyml version of this elementary archetype contract:

elementary.arl
archetype js
variable str : string = ""
entry default(v : string) { str := v }
specification entry default(v :string) {
postcondition p {
str = v
}
}

The generated whyml program has two modules: Elementary_storage and Elementary:

elementary.mlw
module Elementary_storage
use archetype.Lib
use list.List as L
type _storage = {
mutable str : arstring;
mutable _ops : L.list operation;
mutable _balance : tez;
_transferred : tez;
_caller : address;
_source : address;
_now : date;
_chainid : chain_id;
_selfaddress : address;
} by {
str = "";
_ops = L.Nil;
_balance = 0;
_transferred = 0;
_caller = "";
_source = "";
_now = 0;
_chainid = 0;
_selfaddress = "";
_entry = None;
_tr = L.Nil
}
val ref _s : _storage
end
module Elementary
use archetype.Lib
use Js_storage
let default (v : arstring) : unit
ensures {
[@expl:p]
_s.str = v
}
= _s.str <- v
end

Elementary_storage defines the contract storage and all variables available to entrypoints (caller, transferred, ...). Elementary defines entrypoints and their postconditions.

The postcondition p is declared in whyml with the ensures keyword.