Formal verification improves software security by finding bugs and mathematically proving their absence via mathematical methods. Smart contracts are perfect applications for formal verification because bugs are costly, the code is typically small or modular, and it evolves over time.

A common belief among many DeFi projects is that formal verification must come last, after auditing and once the code is stable. Many think that there is little benefit in trying to verify an imperfect code — we know the attempt to get a correctness proof will be futile. Investing effort in securing a temporary piece of code seems like a waste of expensive developer time that does not contribute to the security of the final product. Contrary to these misconceptions, we argue that formal verification should be shifted left to increase both productivity and security.

Shift Left Security is a best practice from web2 software development that ingrains security into the earliest stages of the development process. Vulnerable code is detected and fixed during development rather than after. Shift left security reduces delivery times, as security and development can be worked on in parallel. The earlier an issue is found, the smaller in scope and cheaper its fix. Additionally, tighter security integration throughout the development process leads to better security outcomes.

Lately, security experts in DeFi advocate the use of shift-left security. We argue that formal verification and other tools such as Forge and Echidna are no exception. It is best to start formal verification as early as possible in the pipeline, before any code freezes, and before the code is even feature complete. Shifting left has several benefits unique to formal verification, besides the general upsides.

Thinking of — and formally stating — system invariants before coding clarifies deficiencies in initial designs and guides the ultimate implementation. By starting verification early, you can write code designed for formal verification from the beginning rather than discovering after development that entire pieces require expensive rewrites to make them amenable to formal verification. The most significant value of formal verification tools comes from integrating into CI/CD and running them automatically every time the code changes to ensure no bugs are introduced. This automation reduces errors in the final code, not just its intermediary versions.

Formal verification enables getting the most out of manual auditing that comes after it. Smart-contract audits are expensive and must be scheduled a long time in advance. Not only is it cheaper to find bugs in other methods if possible, but the fewer flaws the code has, the more focused and beneficial auditing will be. Furthermore, auditors can review specifications to ensure that the formal guarantees provided by automated tools match programmers’ expectations. As published research has found time and time again, even power users can make many mistakes in writing specifications.

Formal verification is becoming more and more accepted not just as a helpful tool but as a must-have for smart contract security. Starting formal verification early (and using it often!) is crucial to successfully integrating it into any project.