Some time ago, I was fortunate to be part of the team working on Oyente, a Smart Contract analysis tool for Ethereum. The tool was part of a paper presented at CCS 2016 (Video of my presentation on the paper is below), and was then inducted into the Ethereum codebase.
A write-up I had on Medium (that somehow went viral) about the dangers of smart contract bugs is here.
Oyente was quite successful for its time, flagging over 80% of all deployed contracts as having some form of bug. Some of these have since been patched up through EIPs in the Ethereum codebase, or inducted as part of the analysis conducted by contract frameworks.
I have since then received a fair few queries regarding the status of the project as well as possible upgrades. As of now the project have been taken over by the good folks at MelonPort, who have moved the development repository here. The older version is still active, and if you wish to run research level code at your own risk (perhaps to marvel at the comments of an older age or to build on it yourself), the Docker image is here. I have since been working on a few projects in the Ethereum space and outside, and hope to keep it posted soon. I realise I've been behind with writing up some projects, and I'm hoping to get ahead of it soon.