In practice though, most of the interesting smart contracts can be implemented withverysimplebusinesslogicanddonotneedtoperformcomplexcalculations. Our solution is to cap the maximum number of steps that a program is allowed to run for in a single transaction. Since blocks have a size limit that caps the number of transactions per block, there is also a cap on the number of computation steps per block. This rate limitation foils CPU-usage denial-of- service attacks. Meanwhile, legitimate users can issue multiple transactions to compute more steps than allowed in a single transaction, though at a limited rate. Miners may decide to exclude too long of an execution if they feel the included fee is too small. Since the Tezos protocol is amendable, the cap can be increased in future revisions and new cryptographic primitives included in the scripting language as the need develops. 1.4 Correctness Bitcoin underpins a $8B valuation with a modest code base. As security re- searcher Dan Kaminsky explains, Bitcoin looks like a security nightmare on pa- per. A C++ code base with a custom binary protocol powers nodes connected to the Internet while holding e-cash, sounds like a recipe for disaster. C++ programs are often riddled with memory corruption bugs. When they are connecting to the Internet, this creates vulnerabilities exploitable by remote attackers. E-cash gives an immediate payoff to any attacker clever enough to discover and exploit such a vulnerability. Fortunately, Bitcoin’s implementation has proven very resilient to attacks thus far, with some exceptions. In August 2010, a bug where the sum of two outputs overflowed to a negative number allowed attackers to create two out- puts of 92233720368.54 coins from an input of 0.50 coins. More recently, massive vulnerabilities such as the heartbleed bug have been discovered in the OpenSSL libraries. These vulnerabilities have one thing in common, they happened be- cause languages like C and C++ do not perform any checks on the operations they perform. For the sake of efficiency, they may access random parts of the memory, add integers larger than natively supported, etc. While these vulner- abilities have spared Bitcoin, they do no not bode well for the security of the system. Other languages do not exhibit those problems. OCaml is a functional pro- gramming language developed by the INRIA since 1996 (and itself based on earlier efforts). Its speed is comparable to that of C++ and it generally features among the fastest programming languages in benchmarks[12]. More impor- tantly, OCaml is strongly typed and offers a powerful type inference system. Its expressive syntax and semantics, including powerful pattern matching and higher-order modules, make it easy to concisely and correctly describe the type of logic underpinning blockchain based protocols. OCaml’ssemanticisfairlyrigorousandaverylargesubsethasbeenformalized[13], which removes any ambiguity as to what is the intended behavior of amend- ments. In addition, Coq, one of the most advanced proof checking software is able 9