Comment by seanwilson

I think the problem is that the language for smart contracts that backs Ether hasn't been written with formal verification in mind. You could apply formal methods to anything after the fact but it doesn't look like they've made this easy here. You could claim that a C program could be made bug free eventually by applying formal methods for example but it would require a huge amount of work.

Is there a good reason they didn't use a battle tested pure functional language with a strong and expressive type system?