An incredible opportunity to finally prove the value of Formal Methods

The following post is written as an open letter to formal methods researchers, particularly cryptocurrency outsiders.

Dear formal methods researcher,

I think there is an incredible opportunity for formal methods to finally gain widespread adoption in a high stakes environment: DeFi.

Whether you believe in the goals of cryptocurrency or not – I’m a true fence sitter, neither completely for nor against it – the unique founding assumptions and incentive structures of the space are almost a perfect fit for the use of formal methods.

Even those who concede that formal methods are useful will cite its cost and the time it takes to verify as practically insurmountable obstacles to its widespread adoption. And fair enough. This is true enough for web and mobile applications.

However, three things stand out about DeFi projects.

1. The on chain code is quite small, often on the order of 2000-3000 SLOC and very rarely above 10,000 SLOC.
2. Bugs are exploited in DeFi “smart contracts” on a remarkable frequent basis; several projects a week.
3. The economic damage caused by each of these exploits is usually in the order of millions of dollars, sometimes the hundreds of millions. For a real time list of hacks see DefiLlama’s list of hacks

I’m an ex-Haskeller and have dabbled in Isabelle/HOL and Agda. I’m aware of the superb outcomes of the seL4 project. I’m also aware of the existence of CompCert and some other work out of INRIA. From the moment I heard that Ethereum smart contracts ¹ would be programmed in a Turing Complete language I knew that bugs were going to be an issue.

What’s so fascinating about Ethereum is that even the designers and core developers seem to be largely unaware of much of the progress that has been made in formally verifying systems or even designing systems in a principled manner (so that certain classes of bugs are avoided altogether). What’s even more disappointing is that Cardano, a project written in Haskell and with a System F like core language (Plutus) seems similarly plagued by exploits that could be removed entirely with sufficient formal verification.

The consensus in the web3 community is that auditing and bug bounties will be enough to secure web3. To say I am highly skeptical of this position is an understatement. I’m convinced that many projects are so complex that there is no way all the bugs can be found through informal processes.

To that end, I put some skin the game and became an auditor and, later, a bounty hunter. I learned the basics by doing competitive auditing on a platform called Code Arena and then moved to Immunefi to find projects with bug bounties. A cursory glance will show you that many of those bounties are very substantial.

My original suspicion was proven true. Using purely informal techniques – with a dash of property based testing – I’ve been able to land two large bug bounties. The exploits I responsibly disclosed prevented $1.5M in economic damage to Notional Finance and $100M in economic damage to KyberSwap.

And yet, even though it might seem I’m onto a good thing and should continue down this lucrative career path, I feel this is formal methods time to shine. And I believe an increasing number of people in the DeFi community are receptive. If several multi-million dollar hacks every week are not enough to convince people of this, I can’t imagine what will.

One of the core tenets of DeFi is that users should be able to read the source code of the financial instruments that they are using. However, this means that potential attackers have unfettered access to their inner workings. Fortunately, so do auditors and bounty hunters and so many potential attacks are prevented. However, as stated above, there are still many hacks every week. Auditing and bounty hunting do not seem sufficient.

I feel this is due to the shortcomings of informal auditing processes. Not only that, formal verification is required on the tooling as well. A project was recently hacked because of a compiler bug. Reading the source code of the project, alone, could not have discovered the bug.

People in DeFi are coming to the realisation that unless the correctness issue can be solved DeFi will never succeed. And there are still many true believers in DeFi! Sure, you might be getting a 20% return from a particular project but does that matter if there’s a 50% chance per annum that you lose all your money? Here are some tweets that express this sentiment.

If you’re a cryptocurrency outsider, I understand that you might have reservations about it. Equally, you may not. In any case, it doesn’t matter for the purposes of showing that formal methods could work.

If the results of HACMS can be replicated, if smart contracts can be written that don’t get hacked in the highly adversarial dark forest of DeFi then formal methods will truly have proved its mettle. Personally, I can’t think of a better test-bed for proving its effectiveness.

If you’ve read this far dear formal methods researcher I’d be very interested in your thoughts on this matter and whether you’d like to get involved in one way or another. Please contact me at security shift-2 100proof symbol-to-the-right-of-comma org or DM me on X/Twitter.