Using Formal Verification techniques when auditing

4 min read5 days ago

At Extropy we are continually striving to improve the quality of our audits to help ensure that our clients’ projects are safe from attack. One approach that is proving successful is formal verification. In this article I want to give an overview of the area and illustrate the benefits of formal verification techniques.

Formal verification offers a powerful layer of security when it comes to auditing smart contracts, especially those underpinning DeFi applications. In the high-stakes world of DeFi, where billions of dollars are managed by code, ensuring the robustness and correctness of smart contracts is paramount. Traditional auditing methods, while valuable, can be enhanced significantly by incorporating formal verification techniques.

Understanding Formal Verification

Formal verification is a rigorous, mathematically-based approach to ensure that a system, in this case, a smart contract, behaves exactly as intended under all possible conditions. Unlike traditional testing, which explores only a subset of possible scenarios, formal verification aims to prove the correctness of a system against a formal specification. This specification precisely describes the intended behaviour of the smart contract, often using mathematical logic.

A good analogy is this: traditional testing is like checking if a bridge can hold a few cars by driving a few cars over it. Formal verification, on the other hand, is like using engineering principles and mathematical calculations to prove that the bridge can withstand the maximum load it was designed for, and more, under any circumstance.

Why Formal Verification is Crucial for DeFi Smart Contracts

DeFi smart contracts are particularly vulnerable and attractive targets for exploits due to several factors:

Immutability and Irreversibility: Once deployed, smart contracts are generally immutable. Bugs or vulnerabilities cannot be easily patched, and exploits can lead to irreversible financial losses.
High Financial Stakes: DeFi applications often manage substantial amounts of assets. A single vulnerability can result in the theft of millions, or even billions, of dollars.
Complexity of Logic: DeFi protocols often involve intricate interactions between multiple smart contracts, complex financial logic, and novel economic mechanisms. This complexity increases the likelihood of subtle bugs that are hard to detect through conventional methods.
Transparency and Open Source: While transparency is a core tenet of DeFi, it also means that the code is publicly available for anyone, including malicious actors, to scrutinise for vulnerabilities.

Traditional audit methods, such as manual code reviews and unit testing, play a vital role in identifying common vulnerabilities. However, they are inherently limited by human oversight and the scope of test cases. In complex DeFi systems, these methods may not be sufficient to guarantee the absence of critical flaws. This is where formal verification steps in to provide a more robust and comprehensive security assurance.

Benefits of Formal Verification in DeFi Smart Contract Audits

Integrating formal verification into the smart contract audit process brings numerous advantages:

Uncovers Hidden Bugs: Formal verification can detect subtle vulnerabilities and edge cases that might be missed by traditional testing and manual reviews. By exhaustively exploring all possible execution paths, it can identify flaws in logic that are triggered under specific, and perhaps unexpected, conditions.
Provides Mathematical Certainty: Unlike testing, which can only show the presence of bugs but not their absence, formal verification aims to mathematically prove that the smart contract adheres to its specification. This provides a higher degree of confidence in the contract’s correctness.
Reduces Risk of Exploits: By identifying and eliminating vulnerabilities before deployment, formal verification significantly reduces the risk of costly exploits and hacks. This is crucial in DeFi, where exploits can have devastating financial consequences and erode user trust.
Enhances Trust and Transparency: In a trust-minimized environment like DeFi, formal verification can serve as strong evidence of a protocol’s security and reliability. A formally verified smart contract can instill greater confidence in users and investors, fostering wider adoption.
Cost-Effective in the Long Run: While formal verification can be initially more expensive and time-consuming than traditional audits, it can be highly cost-effective in the long run by preventing potentially catastrophic exploits. The cost of a major DeFi hack far outweighs the investment in rigorous formal verification.

Challenges and Considerations

Despite its powerful benefits, formal verification is not a silver bullet and comes with its own set of challenges:

Complexity and Cost: Formal verification is a complex and resource-intensive process. It requires specialised tools and expertise in formal methods, which can be costly and time-consuming.
Skill Requirements: Performing formal verification requires highly skilled engineers with a deep understanding of formal methods, logic, and smart contract languages.
Scope Limitations: Formal verification is typically applied to specific critical parts of a smart contract or system, rather than the entire codebase. Defining the scope of verification and creating accurate formal specifications can be complex.
Specification Accuracy: The effectiveness of formal verification relies heavily on the accuracy of the formal specification. If the specification is incomplete or incorrect, the verification process may not detect all vulnerabilities.
Tooling and Automation: While tools and automation are improving, formal verification for smart contracts is still a relatively evolving field. The tooling may not be as mature or user-friendly as in other domains.

Conclusion

Formal verification offers a significant advancement in the security auditing of DeFi smart contracts. By providing mathematical guarantees of correctness, it goes beyond the limitations of traditional testing and manual reviews, offering a deeper level of security assurance. While challenges exist in terms of complexity, cost, and expertise, the benefits of reduced exploit risk, enhanced trust, and long-term cost-effectiveness make formal verification an increasingly valuable tool in the DeFi security landscape.

Since 2017, Extropy has been at the forefront of blockchain security, auditing smart contracts across Ethereum and Zero-Knowledge (ZK) protocols. We have collaborated with leading ecosystems, including Base, Starknet, and MINA, ensuring their smart contracts are resilient, efficient, and secure.

We specialize in DeFi, on-chain games, and ZK applications, leveraging formal verification, static analysis, and deep manual reviews to uncover vulnerabilities before they become exploits. Whether you’re working with Solidity, Rust, Cairo, or zkVMs, our collaborative approach ensures your project meets the highest security standards.

- Website: security.extropy.io
- Email: info@extropy.io

Get in touch today — let’s build safer smart contracts together!