The Zilliqa team has been working for quite some time on a static analyzer called Cashflow analyzer. The analyzer takes a Scilla smart contract as an input and checks whether incoming and outgoing money are handled correctly by the contract.
Here is an example of a contract that incorrectly handles money. The cashflow analyzer is able to detect the bug.
In order to try out your cashflow analyzer, build
scilla-checker from source and then call the
scilla-checker binary on the contract file.
To learn more on the topic, give this blog post a read: https://blog.zilliqa.com/introducing-the-zil-cashflow-smart-contract-analyser-ded8b4d84362