Archetype 1.1 and FA1.2 contract

Milestone M1

Last month, we announced the development of the feature to transcode existing smart contracts developed in other languages (i.e. Ligo, SmartPy) to Archetype in order to verify them.

Today, we are announcing that the first milestone (namely M1) is achieved and version 1.1 has been released, which completes the Archetype language with features like the nat type and basic data containers like records, lists, sets, and maps.

This means that it is now possible to manually transcode a contract written in Ligo or SmartPy to Archetype. This feature paves the way for our next milestones, M2 and M3, which will automate the transcoding process.

The dummy snippet example below shows how lists, sets and maps are declared in Archetype:

effect {

  var l : list<nat> = [ 1; 2; 2 ];
  var s : set<string> = [ β€œthis”; β€œis”; β€œa”; β€œset” ];

  var m : map<nat,string> = [ (0, β€œv0”); (1, β€œv1”) ];
  m := map_put(m, 2, β€œv2”);


The methods to access and modify these containers are presented in this documentation article.

Smart contracts library

Additionally, 2 smart contracts have been added to the library:

  • the unanimity contract enables developers to anchor unanimity agreements on numerical values close enough to each other. It’s typically used to anchor an agreement between an electric vehicle power equipment, the car, and the grid.

  • the FA1.2 token whose specification may be found here is the fungible token for Tezos.

Below is the FA1.2 Archetype version:

archetype fa12

constant totalsupply : nat = 10_000_000

asset allowance identified by addr_owner addr_spender to big_map {
  addr_owner : address;
  addr_spender : address;
  amount : nat;

asset ledger identified by holder to big_map {
  holder : address;
  tokens : nat = 0;
} initialized by {
  { holder = caller; tokens = totalsupply }

entry %transfer (from_ : address, to_ : address, value : nat) {
  require {
    r1 otherwise "NotEnoughBalance" : ledger[from_].tokens >= value;
  effect {
    if caller <> from_ then (
      var current = allowance[(from_, caller)].amount;
      dofailif(current < value, ("NotEnoughAllowance", ((value, current))));
      allowance.update((from_, caller), { amount -= value });
    ledger.update(from_, { tokens -= value });
    ledger.addupdate(to_, { tokens += value });

entry approve(spender : address, value : nat) {
  var k = (caller, spender);
  if allowance.contains(k) then (
    var previous = allowance[k].amount;
    dofailif(previous > 0 and value > 0, (("UnsafeAllowanceChange", previous)));
  allowance.addupdate( k, { amount = value });

entry getAllowance (owner : address, spender : address, cb : entrysig<nat>) {
  transfer 0tz to entry cb(allowance[(owner, spender)].amount);

entry getBalance (owner : address, cb : entrysig<nat>) {
  transfer 0tz to entry cb(ledger[owner].tokens);

entry getTotalSupply (cb : entrysig<nat>) {
  transfer 0tz to entry cb(totalsupply);

Several new features of version 1.1 are used in this example:

  • nat literals may now use the big int β€œ_” notation to gather digits by 3
  • an asset may now be identified by several fields, as allowance is identified by addr_owner and addr_spender.
  • an entry point name that conflicts with one of Archetype keyword may still be used by prefixing it with β€œ%”, like %transfer entry in this example (transfer is the instruction to create a transaction)
  • fail instructions (fail, dorequire and dofailif) now take an argument of any type (except assets for the moment) to fail with
  • entrysig is the type of callbacks signatures (more information in this article)

Archetype comes with a rich library of contract examples (~30).

Next steps

Our next milestone is the automatic transcoding from Ligo to Archetype, which should be available by October. In the meantime, we are also refactoring the verification layer in order to speed up and make the verification process easier.


Please refer to the online documentation.

Follow Archetype on twitter for further updates.