The Tezos community provides a rich technical and human eco-system regarding formal verification:
|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|
The Completium contract templates have been formally specified with Archetype.
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.
Archetype generates the contract's code and specification in whyml, the Why3 language.
The following Completium CLI command:
generates the whyml version of this elementary archetype contract:
The generated whyml program has two modules:
Elementary_storage defines the contract storage and all variables available to entrypoints (
Elementary defines entrypoints and their postconditions.
p is declared in whyml with the