to extract OCaml code from proofs. As Tezos matures, it will be possible to automatically extract key parts of the protocol’s code from mathematical proofs of correctness. Examplesofspectacularsoftware failure abound. The heartbleed bug caused millions of dollars in damages. In 2013, a single bug at high-frequency trading firm Knight capital caused half a billion dollars worth of losses. In 1996, an arithmetic overflow bug caused the crash of Ariane 5, a rocket that had cost $7B to develop; the cost of the rocket and the cargo was estimated at $500M. All of these bugs could have been prevented with the use of formal verifica- tion. Formal verification has progressed by leaps and bounds in recent years, it is time to use it in real systems. 2 Abstract Blockchains Tezos attempts to represent a blockchain protocol in the most general way possible while attempting to remain as efficient as a native protocol. The goal of a blockchain is to represent a single state being concurrently edited. In order to avoid conflicts between concurrent edits, it represents the state as a ledger, that is as a series of transformations applied to an initial state. These transformations are the “blocks” of the blockchain, and — in the case of Bitcoin —the state is mostly the set of unspent outputs. Since the blocks are created asynchronously by many concurrent nodes, a block tree is formed. Each leaf of the tree represents a possible state and the end of a different blockchain. Bitcoin specifies that only one branch should be considered the valid branch: the one with the greatest total difficulty. Blocks, as their name suggests, actually bundle together multiple operations (known as transactions in the case of Bitcoin). These operations are sequentially applied to the state. 2.1 Three Protocols It is important to distinguish three protocols in cryptoledgers: the network protocol, the transaction protocol, and the consensus protocol. The role of the meta shell is to handle the network protocol in as agnostic a way as possible while delegating the transaction and consensus protocol to an abstracted implementation. 2.1.1 Network Protocol The network protocol in Bitcoin is essentially the gossip network that allows the broadcasting of transactions, the downloading and publishing of blocks, the discovery of peers, etc. It is where most development occurs. For instance, bloom filters were introduced in 2012 through BIP0037 to speed up the simple payment verification for clients which do not download the whole blockchain. Changes to the network protocol are relatively uncontroversial. There may be initial disagreements on the desirability of these changes, but all parties interests are fundamentally aligned overall. 10