Would executable bitcoin spec reduce consensus bugs?

[Comeacross]

I have been thinking lately about how bitcoin protocol rules are currently specified mostly in the code itself (i.e the Bitcoin core) scattered BIPs and developer documentation. I know this has worked well for about 17 years now but subtle differences in interpretation occasionally pop up between between implementations and even between versions of Core. We've seen edge cases in block acceptance, mempool policy and consensus rules that in theory could lead to chain splits if not caught early.

I came across this post on the Bitcoin dev mailing list and it caught my attention. btc-verified: formalizing the Bitcoin protocol". The idea is to create a more formal, machine readable specification of the protocol. So this got me wondering.

How feasible would it be to have a single, executable reference specification that could serve as a golden model for consensus rules? Could this reduce the risk of consensus divergence, catch bugs earlier and make it easier for alternative clients to stay perfectly in sync?

I'm thinking this would slow down development too much but what other downsides do you foresee?

I'm wondering if investing in a formal executable spec could make the protocol more robust long term especially as the network grows and we consider more complex soft forks.

Sorry if the post is a bit lengthy.

[athanred]

Would executable bitcoin spec reduce consensus bugs?

The answer is: maybe. As always, the devil is in the details. Bugs can be found everywhere: on assembly level, on compiler level, on Operating System level, and in a lot of other places. Even if you formally prove, that the code is correct, then still: it can be always executed incorrectly, because of many reasons. For example: even the perfect program can be halted in the middle of the execution, and then, running it again can lead to some bugs. There are many places in Bitcoin Core, where it trusts the user to not do some nasty things: break that assumptions, and you will have an unsafe system. For example: it fully trusts, that the database, loaded from the hard disk, is correct. However, if you mess up that database, then your client can sign coins in a way, which could allow stealing them.

Some thoughts about theory vs practice: https://unenumerated.blogspot.com/2005/12/bit-gold.html

The main problem with all these schemes is that proof of work schemes depend on computer architecture, not just an abstract mathematics based on an abstract "compute cycle." (I wrote about this obscurely several years ago.) Thus, it might be possible to be a very low cost producer (by several orders of magnitude) and swamp the market with bit gold. However, since bit gold is timestamped, the time created as well as the mathematical difficulty of the work can be automatically proven. From this, it can usually be inferred what the cost of producing during that time period was.

Today, SHA-256 is architecture-independent, and can be executed on any CPU, and people even created ASICs for that. However, still: having a mathematical proof, that the code is correct, will not eliminate all bugs. It can help, but it won't solve everything. After all, we use finite machines with finite resources, which means that everything can always be broken, at some point in time. But of course, many cryptographical primitives may be strong enough, to be resistant to many attacks, for quite long time, which can make it useful.