Quote from: work2heat on January 14, 2015, 09:21:55 PM

Is there somewhere I can read about the kinds of corner cases that were discovered and how they were dealt with?

They're sort of scattered in various places, for example: http://sourceforge.net/p/bitcoin/mailman/message/29699385/

Quote

Also, what would it take to produce a formally verifiable implementation of bitcoin? Is such a thing even possible? Can we expect a PhD thesis to deliver the matter in the next decade?

One question with formal verification is what are you formally verifying? If the question is the most important question in consensus "is this function equivalent to that function for all inputs" there is one very easy to have a strong guarantee that the answer is true: make them be exactly the same function. Formally proving two functions written in different languages compute the same thing is much harder, and likely not practically possible if the languages are very different or the algorithms used internally substantially different.

To formally verify other properties we first need to extract the part that needs to be verified into it's smallest self contained realization. You can look at whats been done with SEL4 to see whats currently possible (and how much work it takes for a rather small program) at the state of the art.

In Bitcoin core we're working on the isolation which is an important first step on both with the "use the exact same code for the consensus critical parts" approach as well as the "formally show some code achieves certain properties". I suspect that on the latter we won't make much progress in the near term outside of some parts in the underling cryptographic code unless some researchers pick it up as an area of study, but we should hopefully be well positioned to take advantage of formal analysis tools as that space matures.