Tools

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

Tools	Description
Michocoq	A specification of Michelson in Coq to prove properties about smart contracts in Tezos.
Archetype	Archetype 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.