The Bitcoin community is a fascinating mixture of political idealists, technology enthusiasts, entrepreneurs, investors and others. One group that's increasingly prominent is distributed systems researchers, attracted to some of the interesting problems around Bitcoin and the blockchain. There's plenty of interesting work to come, but some valuable research has already been done. Much of this work focuses on the theoretical core of bitcoin, and shows real progress towards answering concerns about bitcoin's safety and liveness bounds.
In The Bitcoin Backbone Protocol: Analysis and Applications, Garay, Kiayias and Leonardos write about the core of Bitcoin, which they call the backbone. The argument for the correctness of the core of bitcoin from Satoshi's original paper is far from fulfilling:
The majority decision is represented by the longest chain, which has the greatest proof-of-work effort invested in it. If a majority of CPU power is controlled by honest nodes, the honest chain will grow the fastest and outpace any competing chains.
Garay et. al. attack this core argument directly, and analyze the exact safety and liveness properties of the protocol. The contribution that's going to launch a million online arguments is that bitcoin does not solve the Byzantine agreement problem1:
This is because in case the adversary finds a solution first, then every honest player will extend the adversary’s solution and switch to the adversarial input hence abandoning the original input.
Nakamoto’s protocol does not quite solve BA since it does not satisfy Validity with overwhelming probability.
Their argument hinges on the validity property of Byzantine agreement (or, rather, strong validity 2), and showing that the chosen value may not be one of the inputs to an honest player. In their definition of Byzantine agreement, agreements are only valid if they pick the input of one of the honest players. That doesn't appear to be true of the bitcoin protocol as implemented.
Reducing the practical importance of this result, they also prove a chain quality property. This property puts an upper bound on how often a dishonest player's entry will be added to the chain 3. That's obviously critically important for liveness, and preventing denial-of-service against honest players.
I find this kind of research on Bitcoin very interesting. The community has very strong opinions on the safety and liveness of bitcoin. Until recently, there was little evidence to support these opinions. Proving bitcoin's distributed systems properties is very useful, even though there are still many interesting questions around topics like scalability and economic incentives.