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
https://github.com/bitcoin/bips/blob/master/bip-0050.mediawi...
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.
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.
New altcoins just don't solve the problem of increasing the security of Bitcoin. Schnorr signatures are are great example of not making the cryptographic assumptions stronger (actually making them weaker) while improving the scalability of the system.