Services
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, ...).
Language
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…
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
Ligo
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
SmartPy and SmartPy.io are an Intuitive and Effective Smart Contract Language and Platform for Tezos.
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