Introduction

The only technology that has, time and again, successfully secured safety-critical applications is formal verification ¹. DeFi applications are safety-critical — bugs in these applications can be exploited to cause catastrophic consequences, and unfortunately, there is no shortage of real-world examples demonstrating this. Therefore, the importance of formal verification for DeFi cannot be overstated. Prominent leaders in the DeFi space, like Vitalik Buterin and Anatoly Yakovenko, recognize this. Formal verification should be mandatory for all layers of Web3 including DeFi apps, implementations of consensus protocols, and user interfaces for interacting with the DeFi apps.

What is formal verification?

Formal verification (FV) is a technique for providing security guarantees for software and hardware systems. It complements techniques like testing and fuzzing, which can only sometimes detect bugs based on predefined properties. Similarly, coding best practices and  audits can boost confidence in a program's bug-free status, but they cannot provide any correctness guarantees that certain bugs in the code are impossible for all inputs.

In contrast, FV produces a mathematical proof that the program behaves according to specification across all executions. Furthermore, it can prevent rare bugs due to corner cases in hardware and software systems before production. A classic real-world example is the famous Pentium hardware, where the hardware circuit contained a very rare bug that slept through various testing mechanisms. Indeed, this bug led to the widespread adoption of FV methods in the hardware industry.

FV relies on a specification that formally states the security property a system must satisfy. A good, reusable specification should be general—it should express the intended behavior of the system without being too tied to the specifics of the implementation. For example, a system may require some user, Alice, not to double spend some amount of Ether. A more general specification would instead say that no user can double-spend any coin during the execution. A side benefit of FV is that one gets a better understanding of the system in the process of identifying and writing the desired properties.

Why does Web3 need FV? Do we need to run the extra mile?

For most software systems, testing, quality control, fuzzing (using random inputs to find bugs), and static analysis are good enough — most of them behave reasonably well in the presence of rare errors, and failure typically does not have severe consequences. Runtime monitoring tools are also often good at detecting errors in production, allowing developers to patch issues quickly before they cause significant damage.

Web3, however, is not like other domains, and FV is a must-have in this case for the following reasons:

1. Low Barrier to Entry = Ease of attack: Web3's beauty is that APIs, code, and data are open and accessible to everyone, everywhere. Furthermore, most logic is captured in small, readable programs, making it easy for newcomers to build Web3 applications quickly. Unfortunately, this also makes Web3 a perfect target for hackers.
2. Small programs carry colossal value: The lines-of-code-to-value ratio is often huge for Web3 programs. For example, Uniswap V2 contains 424 lines of code and has handled over $1,074 billion.
3. Huge Reputational Damage: Rare bugs in Web3 applications have already been exploited, leading to billions of dollars in losses. These bugs can have far-reaching consequences for the protocols and cause reputational damage. Aside from negatively impacting token value, it can lead to difficulty attracting users to future projects.
4. Monitoring can be bypassed: Dynamic monitoring tools are not sufficiently fast at detecting incidents in real-time. Many times, the alerts are seen when it’s too late and can always be bypassed by sophisticated attackers, e.g., via private-mempools.
5. Error mitigation is impossible: Protocols cannot mitigate the consequences of bugs without users losing their assets. This is true both for mutable and immutable smart contracts. The public nature of blockchain allows attackers to track messages in social media and code changes. For example, a white hacker identified a rounding error in Balancer V2. The protocol acted responsibly and asked users to withdraw their assets, but millions of dollars were still lost.

Benefits of Formal Verification

1. Guarantees Security Through Mathematical Proofs: FV mathematically proves that code behaves as intended. In contrast, traditional methods like testing and fuzzing can only find bugs if the chosen inputs manifest the bug.
2. Prevents Rare, High-Impact Bugs: FV has been used to detect rare but high-impact vulnerabilities that have slipped past other methods. Examples include the MakerDao invariant violation putting $10 billion at risk, the Balancer V2 insolvency bug, and the Sushi Trident Bug which could have been used to drain the protocol.
3. Ensures Post-Upgrade Safety: Code upgrades can introduce severe vulnerabilities. Euler V1 and Ronin Bridge both suffered nine-figure losses after seemingly minor changes. One way to mitigate this is to integrate FV into the protocol’s build system to ensure security after every code modification.
4. Deepens Protocol Understanding: The process of writing formal specifications forces teams to clarify assumptions, understand what invariants must hold and why, and identify edge cases, leading to better design, simpler code, and precise documentation. 
5. Builds Credibility and Trust Beyond Fuzzing, and Testing: FV signals a commitment to security that goes beyond check-the-box audits. Leading protocols like Aave, MakerDAO (Sky), Lido, Jito, Uniswap, Euler, Morpho, Kamino, and Solana Token Extension rely on it not only to secure their code but also to position themselves as leaders in a “security-first” approach. Insurance providers recognize the reduced risk and are more likely to offer lower premiums.

How does FV fit into your development life cycle?

FV can and should be used by developers and security researchers as early as possible for bug detection in SDLC, as depicted in the picture below. This not only leads to more reliable software but also to simpler design that is easier to extend and maintain.

We recommend integrating formal verification into CI just like compilers, fuzzers, static analyzers, and linters. Companies like Aave have integrated formal verification into their normal CI pipeline, invoking the Certora Prover after every code change. For example, Aave V3 has integrated the Certora Prover into its CI system since March 2022, and every code change is automatically checked.

Q&A about Formal Verification

Q: Can my code still have bugs after FV?

FV provides mathematical proof that the program behaves according to the specification, which acts as a “single source of truth.” If the specification itself does not accurately encode the program's intended behavior, then the FV results cannot be trusted. Similarly, if the specification does not cover some property, FV cannot provide any guarantees that the system will not have bugs due to violation of that property.

Bugs may also occur due to external events like pricing or dependencies on other libraries and infrastructure’s code that were not formally verified. 

Finally, FV tools themselves may have bugs. Some FV tools reduce the chances of this by minimizing the part that must be trusted (called the Trusted Computing Base or TCB). Some work has shown how to formally verify and differentially test formal verification tools themselves.

Protocols can be hacked after FV. The most likely causes are missing specifications, bugs in the dependency on external events such as pricing, and bugs outside the verification scope or even outside the code. Still, FV drastically increases code security in Web2 and Web3.

Q: Does FV replace auditing or fuzzing?

A: No, FV complements fuzzing and auditing in many ways. For example, auditing the specifications can increase confidence in FV's results. Conversely, when FV finds a violation, it typically produces a concrete input that triggers the bug (called a “counterexample”). This input can be used as a test case or a seed for fuzzers to make them more effective. Finally, invariant testing is a good starting point for FV.

Q. What can be tested or proven using Formal Verification?

Formal Verification provides complete path coverage for any given specification. For example, a specification might state that only a bounded number of tokens can be minted in an ERC20 contract. Formal Verification either guarantees that the rules hold on all paths and all inputs or produces a test input that demonstrates the rule violation. 

Q: Who can do FV?

A: Anyone who is curious to understand the protocol and the code and has basic knowledge of programming and logic, including developers and security researchers. FV improves programmer skills.

Q: What is the best time to apply FV?

A: FV should be used early and often, preferably even before the code is written during the design phase. The “FV mindset” leads to simpler, modular design, which makes FV easier to apply.  

Q: Is an FV a one-time thing?

A: No, FV should be part of a system’s CI so that it runs after any code changes. 

Q: How can one check the quality of FV?

A: FV results are only as good as the specification. Therefore, specifications must be checked for issues like vacuity. Synthetic fault injection and mutation testing should also be used to ensure that the specification catches bugs. It is highly recommended that the specifications be reviewed and audited.

Takeaway

In March 2023, a single unchecked bug in a smart contract wiped out $180 million in user funds. Incidents like this are not anomalies, they are warnings that the community must take seriously. Smart contract audits, fuzzing, and testing certainly help, but they are not sufficient.

Formal verification (FV) has come a long way since its inception by Turing in the 1950s. There are now many powerful proof tools for FV, including SMT solvers like Z3, Yices, and CVC5 and Interactive Theorem Provers like Lean2, K, Coq, and Isabelle.

For teams building DeFi protocols, governance contracts, or any mission-critical application with economic risk, FV is a necessity and there is simply no excuse not to use it, given the large number of excellent tools that are available for FV.

[1] References:

https://dl.acm.org/doi/10.1145/780822.781149

https://link.springer.com/chapter/10.1007/978-3-319-41540-6_2

https://www.absint.com/astree/index.htm

https://compcert.org/

https://dl.acm.org/doi/10.1145/2737924.2737958

https://sel4.systems/

https://dl.acm.org/doi/10.1145/3051092

https://github.com/starkware-libs/formal-proofs

https://medium.com/nethermind-eth/clear-prove-anything-about-your-solidity-smart-contracts-04c6c7381402