Formal Verification on Smart Contract

For ethereum, 2016 might be a tough year, the DAO has been stolen 3.6 million ETH, equivalent of $70 million at that time, due to improper contract design. As a result, more and more automatic verification tool for smart contract come out to prevent potentially huge financial loss.

Today, we will be looking at how formal verification tools work on smart contract, how can we use mathematical proof to ensure the quality of program.