2vyper

It offers novel specification construct which enable sound and precise verification even in the presence of unlimited re-entrancy. 2vyper can modularly verify applications consisting of multiple collaborating smart contracts, that is, it verifies each contract independently using only an interface description of the other involved contracts, without requiring their source code. Additionally, it offers a novel verification technique that allows specifying the desired contract behavior in terms of resource transactions, which makes specifications more intuitive and can catch typical errors (such as the one that enabled the DAO hack) by default.

2vyper is open source and available on external page Github.