Archetype contracts are transcoded to mutliple formats for specific services.

Formal verification

Archetype language provides a predefined set of security properties, and enables specifying contract properties with logic formula. Archetype transcodes these properties to the Why3 format (whyml) and Why3 generates proof obligations to be solved by automatic (Alt-ergo, CVC, Z3, ...) or manual provers (Coq, ...).


Archetype enables to get the Michelson (Tezos execution code) version of the contract, by transcoding the contract to the main high level languages available for Tezos : Ligo and Smartpy. Archetype may also transcode to Ocaml for unitary tests, and Markdown for contract documentation.


Security by high-level expressiveness and simplicity.

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

LIGO is a statically typed high-level smart-contract language that compiles down to Michelson. It seeks to be easy to use, extensible and safe.

Learn more

SmartPy and are an Intuitive and Effective Smart Contract Language and Platform for Tezos.

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