Easy Business logic

archetype blogic_demo(holder : address, value : tez, deadline : date)

entry pay () {
  transfer ((1 + 7% * (now - deadline) / 1d) * value) to holder

The pay entrypoint applies a penalty fee of 7% per day beyond deadline. Archetype language provides exlcusive types to easily implement readable business rules: rationals, dates, durations ...

Explicit Execution Conditions

archetype exec_cond_demo(admin : address, value : nat)

entry setvalue (v : nat) {
  called by admin
  require {
    r1: transferred > value;
    r2: now < 2022-01-01;
  effect {
    value := v;

The setvalue entrypoint executes if the sender is the admin, if the transferred amount is greater than value and if it is called before 2022. Archetype provides specific syntax to establish execution conditions so that the contract is easy to read and check.

Clear State Machine

archetype state_machine_demo(value : tez, holder : address)

states =
| Created initial
| Initialized
| Terminated

transition initialize () {
  from Created to Initialized
  when { transferred > value }

transition terminate () {
  from Initialized to Terminated
  effect { transfer balance to holder }

It is possible with Archetype to design the contract as a state machine. Transitions may have guard conditions (like initialize) and effect on the storage (like terminate). State machines are convenient to make the overall process clear and transparent.

Smart Storage API

archetype asset_demo

asset vehicle {
  vin          : string;
  nbrepairs    : nat  = 0;
  dateofrepair : date = now;

entry repair_oldest () {
  for v in vehicle.sort(dateofrepair).select(the.nbrepairs = 0).head(3) do
    vehicle.update(v, { nbrepairs += 1; dateofrepair = now })

The repair_oldest entrypoint increments the nbrepairs field of the 3 vehicles with oldest date of repair, and with a number of repairs above zero. An asset collection provides a rich API to read/write data (add, remove, update, addupdate, ...), and to iterate over the collection (select, sort, sum, head, tail, ...).

Formal Specification

specification entry repair_oldest () {
  postcondition p1 {
    0 <= vehicle.sum(nbrepairs) - before.vehicle.sum(nbrepairs) <= 3

The postcondition p1 of repair_oldest entry point specifies that the difference between the total number of repairs after the entry point's execution and before, is less or equal to 3. Archetype provides a full-featured specification language for contract invariants and entry point postconditions.

Formal Verification

Archetype transcodes the specification to the Why3 format (whyml) and Why3 generates proof obligations to be solved by automatic (Alt-ergo, CVC, Z3, ...) or manual provers (Coq, ...).


Security by high-level expressiveness and simplicity.

Nomadic Labs Research Seminars #10

High-level smart contract design & verification with Archetype

Benoit Rognier, CEO co-founder at Edukera.

Watch the video

Archetype, a DSL for Tezos

Archetype is a domain-specific language (DSL) to develop smart contracts on the Tezos blockchain, with a specific focus on the formal verification of the contract. Archetype is funded by the Tezos Foundation and developed by Edukera…

Benoit Rognier, CEO co-founder at Edukera.

Read the Article

Verify a smart contract with Archetype

In this article, we develop a smart contract with the Archetype language which enables us to formally verify it in order to find and fix bugs and make sure it complies with its specification…

Benoit Rognier, CEO co-founder at Edukera.

Read the Article


Language features, API reference, and contract library.

Learn more


Archetype is open source. Please join the project.

Go to our Github

VS Code extension

This full-featured Archetype extension provides the standard experience you may expect for professional development.

Compiling errors, commands for Archetype transcoder, ...


We are grateful to be part of the very active and dynamic Tezos community.


Tezos is a new platform for smart contracts and decentralized applications. Tezos is formalizing blockchain governance.

Learn more
Tezos Foundation

The Tezos Foundation stands as part of the community in support of the Tezos protocol and ecosystem.

Learn more
TQ tezos

Tocqueville Group (TQ) works to advance the Tezos ecosystem by helping companies build on Tezos, creating open source software, and connecting the community.

Learn more
Tezos Southeast Asia

Tezos Southeast Asia is the official regional community for advancing awareness and commercialisation of Tezos' smart contract technology in Southeast Asia.

Learn more
Nomadic Labs

Nomadic Labs currently focuses on contributing to the development of the Tezos core software, including the smart-contract language, Michelson.

Learn more

Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions.

Learn more