Hacker News Reader

Manticore in the post above uses formal methods to verify contract properties!

https://github.com/trailofbits/manticore

Ethereum contracts are effectively Turing complete (well, technically linear bounded automata complete). But you get the same state space explosion issues as with formal validation of any other language.

https://github.com/OpenZeppelin/zeppelin-solidity

As much as they use 'secure' in their README, I don't see any real evidence of that in their code.

When I'm looking for formally methods, a package.json is a bad sign.