This is the translation of an interview in French of Vincent Botbol:

Tezos: a 232 million dollars cryptocurrency


In July 2017, Tezos makes a remarked entrance in the world of cryptocurrencies: it attracts 232 million dollars at its launch. Fad or real innovation? Only time will tell… It is clear however that the Tezos blockchain is different from its predecessors and uses cutting-edge technology, supported by strong links with academia. Vincent Botbol, who was recently awarded a computer science PhD at Sorbonne Université, works on the development of Tezos in Nomadic Labs. He will guide us into the world of Tezos which aims to be a formally verified, equitable and sustainable blockchain.

Binary: Why a new currency?

Vincent: A white paper (position paper, white paper), published in 2014, identifies the issues with crypto-currencies like Bitcoin and Ethereum, and defines the principles of a new cryptocurrency, more equitable and more reliable. A prototype is done by OCamlPro, a company specialised in developing software in the OCaml language. OCaml is a programming language born in France and designed to be clean and rigorous. And in 2017 the Tezos project is launched.

Binary: Why did the Tezos project seduce so many people?

Vincent : Tezos solves various problems of Bitcoin. For instance Tezos was designed to be fair between token holders, and to avoid wasting computing resources. The system used by Tezos is named Proof-of-Stake: it is a way to reach a distributed consensus between users – the Tezos holders, who validate the transactions. Another issue is that Bitcoin consumes a lot of energy, incentivising people to buy dedicated servers. Tezos avoids this computing power waste. I believe what seduced so many people in Tezos is it doesn’t consume as much energy as Bitcoin and Ethereum. With the increasing popularity of Bitcoin and Ethereum, the energy consumption has gone out of control. Digiconomist computed that their energetic consumption is similar to that of Ireland. And all that creates a bias in favour of those having access to cheap electricity and cheap hardware.

Binary: How does Tezos avoid the energy waste?

Vincent: Cryptocurrencies modelled on Bitcoin require people to make complex calculations to make money. But most of those calculations have absolutely no use. They are just a random selection of numbers until one fits!

The useful computations are those that verifying the validity of a transaction: when Alice wants to send money to Bob, this transaction is added into a block. Then a validity certificate is added to the block. This guarantees the transaction is correct (for instance, the right amount of money is withdrawn from Alice and credited to Bob). Because those operations are useful and consume some computing resources, block producers naturally receive a fee in Bitcoins, in exchange for their work.

But how to define which user will produce a block and collect the fee? In Bitcoin this problem is solved with a computing race : an artificial mechanism is added to make the computations hard. The first user to finish this hard computation can then produce a block and get the fees. The issue is that the useful computation is made very hard just as a tie-breaker. As a result, when the number of users increases, harder and useless computations need to be added to the system. As bitcoin mining is becoming more and more profitable, people are incentivised into using more computing power to create blocks, and that is wasting energy. The idea in Tezos is to keep only the useful part of that computation – the cheap transactions.

Binary: As a result the Tezos blockchain is not the same as Bitcoin?

Vincent: Not completely. The blockchain principle remains, a decentralised ledger of transactions that allows knowing who owns what. Similarly, blocks are created by users. But to avoid useless computations, Tezos uses a different mechanism than Bitcoin. Instead of organising a computing race, Tezos picks a single user for him to create a block. With a given probability, each user may receive blocks to be created and collect the corresponding fee. That’s how only the useful part of the computation is kept.

Binary: The choice of the block producer is random?

Vincent: Yes, random, with a probability that depends on the number of Tezos tokens the user holds. The more tokens a user holds, the higher the likelihood to be requested to create a block and collect the fee.

Binary: In that case rich users become richer? Why that choice?

Vincent: The idea is to reward the Tezos token holders and get them invested in the success of the token, in proportion of their holdings. The more tokens a user holds, the higher his incentive that everything works flawlessly. As a result, in Tezos the token holders are favoured, instead of those that own computing farms specialised in making those useless computations. At the end it is a form of savings: you get money in proportion of how much you hold.

Binary: You have a PhD in computer science and you are a Tezos developer. How does someone transition from scientific research to blockchains?

Vincent: The two sides are not that far apart. A significant part of the work done in Tezos fall within scientific research. Unsurprisingly, Nomadic Labs, one of the companies that participates in the development of Tezos, hires mainly PhDs and assistant professors. The Tezos Foundation, which manages the funds collected, provides numerous grants for research projects aimed at solving problems of interest for Tezos. It is another way in which Tezos is unique: its creators from the beginning aimed at creating a system which reliability is absolute. More than reliable actually, certified as not having any bugs. When you use a currency, you really want to be able to completely trust the programs that manage transactions. And certifying that a program has no bugs uses formal verification methods, something that is still largely a research topic.

Binary: Could you explain how this works?

Vincent: First at the code level, the source-code of Tezos is open source (available on Gitlab). Like in any blockchain there are bugs which are identified and fixed as the project advances, but unlike Bitcoin, the users can vote for new features. For instance, if Tezos users want to add a patch allowing notarised transactions, the whole community can vote (or delegate its vote) on this addition of feature. If enough people approve the feature, it will be added into the system. In the same way new blocks are validated by Tezos users, new features – including those that may change the Tezos core economic protocol – are approved by the users.

Binary: Alright, but you were talking about a code certified without bugs?

Vincent: Sure. We want to formally verify all the code. That is one of the aspects of the project I like the most. In my PhD thesis I worked on abstract interpretation, which are techniques that allow formally proving that some types of bugs don’t occur in a piece of software – without even running the software. What is difficult in software verification is analysing all the possible outcomes of the software and all the paths the software used to get there. Checking ONE path is easy, just run the software on some data. But how to check ALL paths? Actually, the problem is known to be undecidable (impossible to solve). Ouch! Instead of trying to check all paths, what abstract interpretation does is checking groups of paths which sometimes contain ‘fake’ (impossible) paths in addition to the real ones – but at least we know it contains all the real paths. If we are able to compute those groups of paths and check they remain within controlled values (for instance, not to high), then we have proved the program has no bugs. Or at least that it cannot reach those forbidden values.

For instance, it is easier to check that a variable in a program will always remain positive, than to find all the values it can take in all executions of the program. That information may be enough to prove the absence of bugs, if the variable represents a bank account, and one wants to prove we are never spending more money than available in the account.

Binary: In other words, if we are able to define what a bug is, we can avoid them?

Vincent: Well, it is not that simple. First, defining what a bug is, is a complex question. In order to apply formal verification methods, you need to express the bug in some form of logical language. But many bugs happen because programmers never even imagined the faulty situation could even happen, and never expressed it in any form.

Binary: And if a bug can be expressed beforehand, does it make finding it easy?

Vincent: Still not that simple. First computing groups of paths automatically is difficult. Then what sometimes happens is that the group of paths goes through forbidden values, but when looking at the paths individually, it’s a ‘fake’ path that intersects the forbidden values while the real ones don’t. As a result, it is important to compute precise approximations of the paths – but computing precisely the groups is undecidable as we said before. That’s why automatically verifying large and complex codebases as the one of Tezos is still a research problem. However, the way programs are written also matters. Tezos was written in a way that makes applying formal verification methods easier. And here I only talked about my specific research area, we also use other methods that complement it.

Binary: And the end, what can you do with 232 million dollars?

Vincent: It was somehow complicated at the beginning, and the Tezos world had to overcome some tensions that didn’t make development easy. Things have stabilised now. The funds are managed by the Tezos Foundation, based in Switzerland and provides grants to other organisations for code and ecosystem development. Tezos code being open-source, anyone can participate in its development. Nomadic Labs, the company I work for, is one among many organisations that have received Tezos grants.

Interview done by Charlotte Truchet, assistant professor in computer science at the University of Nantes.