Formal methods are good and all, but you can still run into trouble when you fail to account for everything. Some years ago, I had to work on a massively distr

Formal methods are good and all, but you can still run into trouble when you fail to account for everything. Some years ago, I had to work on a massively distributed system that scaled up or down with minimal communication between nodes, depending on the amount of work the system had. The developer of that scaling algorithm, a mathematician that gives quite a few software talks, and writes books teaching functional programming, wrote a proof for the system, guaranteeing its upper and lower bounds of performance. I was brought in because the system wasn't acting anywhere near those parameters: The worst part was that often it'd not downscale at all. The mathematician pointed at his proof, and therefore at the fact that if there was a problem, it must be a bug somewhere else. So after learning how to read his proof, executing it, and doing all the typical ops stuff to identify what the system believed was going on at any particular time, it became clear that the proof had a significant flaw: It believed that the amount of work that the system received was perfect information, with no latency. Since the real world has latency, and none of that was accounted for, the proof was guaranteeing success in a universe that is different from ours. Once I modified the model to represent the real information quality, the outcomes were pretty close to what we were seeing in reality, and equally unacceptable. So proofs are powerful, and maybe there are zero issues in the proof of this smart contract, but formal models and proofs can still fail you, they'll just fail far less often than your typical system made with unit tests and chewing gum.