# The Devil In The Details

Casanova has something that is surprisingly uncommon in the modern blockchain world, even among the most popular consensus algorithms: mathematically rigorous proofs that the algorithm is safe and that it can make progress under adverse circumstances. In the academic literature, these two properties are called safety and liveness. Before blockchain came around, every serious consensus algorithm came with these proofs. The math is rigorous, and these algorithms are extremely resilient.

Bitcoin started with a radically new approach to consensus which we now call proof of work. Since these ideas power both Bitcoin and Ethereum today, we can see how effective Nakamoto’s ideas were. It genuinely revolutionized the whole field of consensus. Interestingly, in contrast to all the previous work in consensus, the Bitcoin Whitepaper only gives a sketch of a good, mathematical proof of safety and liveness. In that way, it departed from what we call “classical” consensus by hand-waving away the more precise mathematical details.

As we can see in practice, Nakamoto’s original consensus algorithm genuinely works. As a mathematician looking at the sketch of the proof he gave, I find it convincing that we could stick it into the formal, rigorous, theoretical framework that classical consensus uses to prove all of its theorems, and that we could make the proofs rigorous and great. Despite this, however, I think it a fundamental error that Nakamoto, and many of his successors in the blockchain world, have not included mathematically rigorous, complete proofs of safety and liveness.

I appreciate that from a non-mathematician’s perspective, this probably sounds like I’m just fussing about little theoretical details that don’t have practical implications in the real world. I will be the first to say that when I read the Bitcoin Whitepaper for the first time, I read the proof sketch, found it convincing, and didn’t think any more of it. However, as I’ve been doing research within the field of consensus, I’ve seen that this lazy, hand-wavy approach comes with serious disadvantages.

The most obvious of these is that algorithms that don’t come with proofs are almost always vulnerable in some way. Without a proof you don’t know what assumptions about the network have to be true for your algorithm to work, you don’t have a good grasp on pathological scenarios that a hacker could exploit, and you don’t know how many malicious agents your network can tolerate.

This might sound like a theoretical problem, but this has real consequences in the form of attacks, most notably on Bitcoin and Ethereum—one of them in the not so distant past. And prominent researchers, including members of Ethereum’s most advanced research teams, have been making categorically false claims about just how safe and live a consensus algorithm can possibly become. This lack of rigorous math has cost people millions of dollars, both in research expenditures and loss to hackers!

A related disadvantage is that the engineers and mathematicians building the blockchain lose out on some important understanding if they don’t go through the rigorous math. Many of these attacks, in particular on Bitcoin and Ethereum, have to do with something called finality. Finality asks when you can know that a block is never going to change or get overwritten, no matter what. We care about finality because if I want to spend some money deposited into my account, I should be sure that the deposit won’t be overwritten somehow after I spend the money, causing me to overdraft my account.

Finality is intimately related to safety since safety is the property that a finalized transaction will never be overwritten. Bitcoin’s argument for safety says that the longer you wait, the more likely it is that your transaction is finalized. The problem is that within Bitcoin and Ethereum, you can never actually know that your transaction is finalized. Even though the longer your transaction has been recorded in the blockchain, the less likely it is to ever be overwritten, you can never be absolutely sure.

In Casanova, we addressed these issues. We have proofs of safety and liveness that are as strong as any proof in the pre-blockchain consensus world. We talk in detail about our network requirements, about required assumptions, and about exactly when you can know a transaction has completely finalized. By doing this, we prevent many of the attacks that exploit the vulnerabilities of many current blockchains.

The advantage to this is clear: we know exactly what network conditions we need to make Casanova safe and live. We can get a clear picture of potential attacks and plan effectively to prevent them. We can tell when a transaction immutably becomes part of the blockchain, and we can set up incentive structures to make it extremely fast. In this way, we are trying to encourage our fellow blockchain-ers to harken back to pre-blockchain consensus and make sure the algorithms we produce are as thoroughly grounded in rigorous mathematics as those are.