I'm sorry you took offense. My intention was not to slight you, how can you have time to study everything in the world? W.r.t. to the proofs in the paper, they

I'm sorry you took offense. My intention was not to slight you, how can you have time to study everything in the world? W.r.t. to the proofs in the paper, they happen within certain assumptions, assumptions that do not hold when the attack is as I described because the majority will be byzantine! The key idea in the argument is not computer science but economics. If you can earn more we have to assume you will do that (charitable behavior exists but is not a good thing to rely on for security) the issue is that PoS is vulnerable to the tragedy of the commons in a similar way to democracy (the amount of influence each person has is small but time investment of being a rational voter big, hence it is rational to be ignorant - in PoS setting the idea is that you defecting is unlikely to change things so the bribe does not need to be big). Once you've obtained a majority you can censor the minority. How much you can do with your soft fork depends on the chain in question but in general the very fact that you can stop byzantine behavior works against you when the majority is malicious. The reason we cannot do the same in proof of work is because of how expensive the bribes are. Anti-sybil based in racing is hard to censor but when you start voting you can do bullying. Regarding formal verification, you can formally verify the algorithm, implement it safely and still it will not work in the real world due to the game theory considerations. However bittorrent worked and that was largely charity. Similarily the data availability problem has not been a problem (e.g. all bitcoin blockchain is accessible even though there is no monetary incentive to make the archive accessible). While there is no way to exploit known vulnerabilities they may as well not exist. From our exchange you have been appealing to authority but I suggest working through the math and looking at tragedy of the commons. Since you are intimately familiar with how proof of stake works you will be able to convince yourself one way or the other.