“Tezos is a Technology
…implemented in a software project
…which allows participation in a peer to peer network
…that produces a blockchain
…which maintains a decentralized ledger
…instantiating a cryptocurrency. “
-Arthur Breitman
Source: Arthur Breitman discusses Tezos, proof-of-work and smart contract models
That’s the definition given by one of its founders, Arthur Breitman. Tezos is more commonly known as a decentralized blockchain platform that was launched in 2018 and could fit as a third-generation blockchain. The platform was designed to be highly modular, which allows for easy upgrades and changes to be made to its underlying protocols.
This article will cover some of the core concepts that are essential for understanding and developing on the Tezos blockchain.
What Makes it unique:
- Open Source
- Self-amendment
- Governance
- Liquid Proof of Stake
- Formal Verification(Michelson)
Open Source
Although not uncommon in public blockchain projects, it is extremely important to mention that one of the main objectives of blockchain is decentralization. Open source is a method of keeping development transparent and public, which aligns with this objective. Tezos is mainly developed using the OCaml language and uses GitLab as its version control platform while maintaining a GitHub mirror.
Self-amendment
The most important element to discuss in this introduction is self-amendment. It is a crucial concept to understand while developing in the Tezos ecosystem since processes, commands, and even some documentation may become deprecated according to the active protocol. The Tezos mainnet protocol continuously evolves, thanks to the self-amendment process. One of the biggest concerns in Tezos’ design is achieving consensus on the protocol and avoiding hard forks.
This process takes place on its blockchain through governance, which we will talk about later.
Governance
Legitimacy often distinguishes what has value from what doesn’t, and in blockchain, there is a problem of determining legitimacy in evolving and open-source technology. This is where hard forks come into play, and the question arises of how to choose the right fork or the legitimate one. Tezos solves this problem through an on-chain governance process, allowing it to evolve with a verifiable consensus.
This unique governance is described as an on-chain mechanism for proposing, selecting, testing, and activating protocol upgrades without needing to use hard forks. This allows for a transparent, democratic, and decentralized process for making changes to the Tezos blockchain, with token holders able to vote on proposed changes and upgrades.
So, can there be hard forks on Tezos? And how do they prevent people from creating hard forks? The answer is yes, there can be hard forks on Tezos, and nobody can stop anyone from creating a Tezos fork. However, what matters is what the Tezos community considers as the legitimate active protocols, which are defined through governance.
Liquid Proof of Stake
Tezos has created its own consensus algorithm called Liquid Proof of Stake, intended to address problems from its predecessors: “Proof of Stake” and “Delegated Proof of Stake”.
How does it work?
Similar to Delegated Proof of Stake, token holders in Liquid Proof of Stake can delegate their validation rights to other users (validators) and still retain their token ownership. Validators are rewarded for their actions. The main differences between DPoS and LPoS are that the number of validators in a DPoS is fixed to a small number, usually between 20 and 100. In LPoS, this number is dynamically limited by the roll size (token amount entry barrier), and unlike DPoS, any user can become a validator if they have enough coins.
In Tezos, “miners” or “validator nodes” are called Bakers, and Bakers can:
- Bake (Create) new blocks
- Endorse blocks (agree on blocks)
- Participate in the on-chain governance process
In the baking process, bakers are chosen “randomly” (Since Tezos runs a deterministic protocol, there is no actual randomness) but have a priority system to increase the likelihood of a baker being selected according to their tez rights holdings.
Bakers have a minimum entry barrier of one roll, which represents a quantity of tez. Currently, a roll represents 6,000ꜩ. Therefore, the more rolls a person has, the higher their chance of being selected in the priority list to bake blocks. If a baker has missed an endorsement or baking within the time limit, the right to bake passes to the next baker.
Anyone can become a baker, and if a tez holder doesn’t want or can’t become a baker, they can delegate their rights to a baker and switch delegation to any other baker whenever they want. This increases decentralization and promotes participation, where ordinary users are not excluded from the activity.
There are platforms dedicated to rate/list bakers, like baking bad, tezos-nodes, tzstats.
You can find more on this topic here:
Open-Tezos – Liquid Proof of Stake
Formal Verification (Michelson)
Traditional testing, which is also code, could contain bugs, be incomplete, or might not run with a sufficient range of values. There could be countless ways to fail in the implementation. Formal Verification, using formal methods of mathematics, proves or disproves that a program respects its formal specification.
Anyone developing smart contracts will tell you that once a smart contract has been deployed on a public blockchain, it is almost impossible to rewrite or remove it from the blockchain. What some may do is advise users to use a newly deployed version. However, this can be a problem when dealing with DeFi smart contracts or other critical code that interacts with high-value assets or information.
Formal Verification consists of defining the specifications of a computer code, describing what the code must do, and proving that its execution indeed does what it was designed to do. Michelson was designed to allow formal verification.
Here are the elements of formal verification:
- Code:
Smart Contract (Michelson code)
- Formal Specification:
What code must do, not how to do it. What should and shouldn’t be the outcomes of the program, along with its invariants, failures, and postconditions.
- Formal Verification Tool:
Formal Verification converts both the code and the formal specification into a mathematical model. This model is then checked against each other by mathematical proof, resulting in a formal proof that is published for anyone who wants to verify it.
There are specific guidelines to write the formal specification of a program according to the tool used to generate the proofs.
For more information about formal verification, you might want to check:
Available Documentation:
As mentioned before, searching for the right information is a big part of the development process, here are a few sources for searching for documentation:
Advice for developers
Don’t focus too much on Blog Posts
When trying to solve a problem and the documentation is unclear or there’s a concept that is not fully understood, it might be tempting to read blog posts about the subject. However, since it is an evolving protocol, what a developer or influencer describes may not apply to what is currently implemented. This can be problematic.
If you do read blog posts, keep in mind that it can be a great way to learn the whole process, but you have to search for the most updated information.
Join the communities and learn
Joining the communities is the most effective way to stay updated with the most recent implementations and is the best way to learn and practice what you have learned.
In conclusion, Tezos is a highly modular and flexible blockchain platform that uses a Liquid-proof-of-stake consensus mechanism, supports smart contracts and on-chain governance for protocol proposals and updates as part of the self-amendment process, and employs formal verification to ensure the correctness of its smart contracts. Understanding these core concepts is key to developing on the Tezos blockchain.
Did you know all this about Tezos? What feature do you think is the most important? Let us know!