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 })
done
}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, ...).
Papers
Security by high-level expressiveness and simplicity.
Nomadic Labs Research Seminars #10
High-level smart contract design & verification with Archetype
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…
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…
VS Code extension
This full-featured Archetype extension provides the standard experience you may expect for professional development.
Compiling errors, commands for Archetype transcoder, ...
Community
We are grateful to be part of the very active and dynamic Tezos community.
Tezos
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
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