[nmca]

Formal analysis will help sort this out. Larry Paulson trained up these guys: https://www.imandra.ai/

And similar tech can be applied to smart contracts. Would have spotted the DAO bug. Not ready for prime time yet, but will be around the same time as sharding maybe...

[jude-]

That's much easier said than done. If formal methods were practical, we'd be using them already everywhere else.