[dranov]

I agree, and there are efforts to develop formally verified implementations of Nakamoto consensus (which I'm involved in). We've published a paper a year ago about our efforts and first results and I'm currently extending that work for my Master's thesis. Others are also building on top of that work [3].

We're nowhere near having a verified Bitcoin implementation (much less verifying the existing C++ implementation), but we're making steady progress. One could reasonably expect having a verified, deployable implementation in 3-4 years if people continue working on it.

It remains to be seen whether people would switch to that from Core (very unlikely) or Core would adopt it as a component to replace its existing consensus code (interesting possibility, but also unlikely).

[1] - https://github.com/certichain/toychain

[2] - http://pirlea.net/papers/toychain-cpp18.pdf

[3] - https://popl19.sigplan.org/track/CoqPL-2019#program

[iso-8859-1]

First you mention Nakamoto consensus, then you mention "existing consensus code". Are you including Bitcoin script when you say consensus? It seems like a huge task to formally model the whole consensus system, including OP_CODESEPARATOR. How would you replicate something like the BIP-0050 problem?

https://github.com/bitcoin/bips/blob/master/bip-0050.mediawi...

[dranov]

> Are you including Bitcoin script when you say consensus?

Currently, no. Our model considers "consensus" to be agreement on the ordering of transactions. We don't yet interpret the transactions.

However, agreement on the state follows directly provided nodes have a function (in the "functional programming" sense), call it `Process`, that returns the current state given the ordered list of transactions. If all nodes have the same the function, they will have the same state.

The BIP-0050 issue (in my understanding) is that different Bitcoin versions had different consensus rules, i.e. their `Process` functions were different. As far as I know, Bitcoin script is deterministic, so it should be possible to define it functionally. We haven't begun looking at this, though, and I don't know of anyone that has -- some people are working on verified implementations of the EVM, however.

> It seems like a huge task to formally model the whole consensus system, including OP_CODESEPARATOR.

It is a huge task, yes, but it can be done modularly such that reasoning about script interpretation can be almost entirely separated from reasoning about Nakamoto consensus. (This is a bit subtle, since the fork choice rule needs to check if blocks are valid, which relies on script interpretation.)

I don't really understand OP_CODESEPARATOR. As long as it is deterministic, it shouldn't be an issue.

[xiphias2]

It looks interesting, but I believe even verifying 100-200 lines in the real Bitcoin consensus code is more useful. All the Bitcoin Core developers know that the Bitcoin implementation is a mess, but they understood that it's just not going away. As for Bitcoin script, there's a plan to upgrade it to Simplicity (https://blockstream.com/simplicity.pdf), but even then, the old code will stay (there's a concensus that there won't be any hard forks for a long time unless it's really needed).

The last bug was in the caching code (a transaction could slip twice in a block which could lead to inflation), and it was something that only formal verification of inflation in the current code would catch.

My biggest worry is with digital signatures in the Bitcoin blockchain: if there's a bug in it, it's over, building trust again is extremely hard.