Security analysis of Solidity code is now available as a feature in the solidity online IDE called Remix. The code is analyzed for vulnerabilities and reported in the Analysis tab of the remix IDE:
Remix IDE analysis options
A sample output of the same contract with reentrancy bug is shown in the bottom of the preceding screenshot.
This tool analyzes several categories of vulnerabilities including, security, gas, and economy. As shown in the preceding screenshot the analysis tool has successfully detected the reentrancy bug, details of which are shown at the bottom of the screen.
Why3 can also be used for formally ...
