Beyond Tests and Assertions: Can Formal Verification Make DeFi Safer?

As of September 2024, over $200 million has been lost to hacks and exploits on the Ethereum blockchain alone, according to data from Immunefi​ (Cointelegraph). This staggering figure highlights the urgent need for robust security in DeFi protocols, where $38 billion is currently locked in smart contracts across various chains​ (DefiLlama). These hacks often target vulnerabilities in the code, and while traditional code audits help identify such weaknesses, they are not foolproof.

As a DeFi user, continuously exploring new narratives and testing emerging protocols like EigenLayer and Pendle, I became increasingly curious about the safety and risk management aspects of these investments. This curiosity led me to dig deeper into understanding how the code underlying the leading DeFi protocols (AAVE, Compound, MakerDAO, etc) safeguards users’ assets.

This article explores formal verification, a method that mathematically proves system correctness, and how it can significantly enhance security in DeFi protocols. It is particularly relevant for:

• Blockchain developers looking to enhance their code security practices
• DeFi power users and investors who want to understand auditing and general fund security measures
• Protocol operators seeking to improve their security infrastructure
• Governance committee members who need to make informed decisions about protocol upgrades and security measures
• Auditors looking to expand their toolkit with formal verification methods
• Researchers, educators, and students interested in advanced security techniques for cybersecurity and blockchain
• Regulatory bodies and insurance providers in the DeFi space who need to understand and assess protocol risks

This article offers an in-depth look at formal verification in DeFi. As it’s a bit of a long read, here’s a friendly guide to help you navigate the content, with notes on who might find each section most relevant:

• The Limitations of Traditional Testing: Explores why conventional testing methods might not be enough for DeFi protocols. For all readers, especially those new to DeFi security.
• The Case for Formal Verification: Introduces how mathematical proofs can enhance smart contract security. For DeFi users, investors, and anyone curious about improving protocol safety.
• Formal Specifications and Symbolic Variables: Explains the building blocks of formal verification in simple terms. For developers and technically inclined readers.
• Practical Example: From Code to Proofs: Walks through a step-by-step verification process, great for those who love technical details. For developers, researchers, and those deeply interested in the mechanics.
• Certora Prover: Showcases a powerful tool that automates formal verification for smart contracts. For developers and protocol teams considering implementation.
• Challenges and Applicability: Discusses where formal verification fits in the DeFi landscape and its current limitations. For protocol operators, governance members, and researchers.
• The Interconnected Nature of Security Measures: Puts formal verification in context with other security practices. For all stakeholders to understand the bigger security picture.
• The Importance of Reputable Verification: Offers tips for evaluating the security of DeFi protocols you might use or invest in. For DeFi users and investors.
• Conclusion and Resources: Wraps up key points and suggests further reading for the curious. For all readers, with resources for those wanting to dive deeper.

We can all contribute better to a safer DeFi ecosystem by understanding formal verification and advanced security practices.

The Limitations of Traditional Testing

Traditional testing methods focus on verifying code behavior in specific, predefined scenarios. These methods include:

• Unit tests: These tests check individual components or “units” of code for correctness, ensuring each part works in isolation.
• Integration tests: These verify that all system components work together correctly.
• System tests: These cover end-to-end testing to ensure the entire system operates as expected.
• Runtime assertions: These checks are performed during execution to verify that certain conditions hold while the program runs.
• Fuzzing: An automated testing technique that inputs invalid, unexpected, or random data into a system. It’s effective at finding edge cases and vulnerabilities that conventional tests might miss.

While these testing methods are useful, they come with notable drawbacks:

• Limited scope: Traditional tests only validate specific cases or executed paths. They don’t cover all possible states the system could enter.
• Missed edge cases: Rare and unexpected combinations of inputs or system states can often go untested, leading to hidden bugs or potential system failures.

As a real-world analogy: Testing a ship only in calm waters doesn’t guarantee its performance in a storm. Similarly, code that passes all predefined tests may still fail in unpredictable, real-world scenarios.

Traditional test coverage tools provide metrics on the percentage of code covered by tests, but they don’t verify every possible state of the system. What we want is a more comprehensive solution that mathematically proves the legality of every state the system can enter, regardless of the specific test paths.

As Vitalik Buterin famously said, “Code is law” in the decentralized world. This means that any flaw in a smart contract is essentially a flaw in the system itself. By all means protocol developers must ensure that this “law” behaves as intended, catching potential bugs or vulnerabilities before they can be exploited.

The Case for Formal Verification

Here comes a more rigorous approach that operates and guarantees far beyond traditional testing:

• Exhaustive Validation: Instead of checking specific scenarios, formal methods ensure the system behaves correctly in every possible state.
• Proof of Security: It mathematically guarantees that the system won’t enter any illegal or unintended states — crucial for DeFi protocols handling billions in assets.
• No Missed Edge Cases: Every potential interaction is covered, leaving no room for untested vulnerabilities.

By moving from just “catching bugs” to proving correctness, formal verification aims to guarantee that smart contracts behave, even under complex conditions.

Formal Specifications

We need a way to define a system’s behavior as a clear set of rules to verify its correctness. This is where formal specifications come in, serving as the foundation for formal verification. These specifications define how the system should remain secure, predictable, and behave correctly under all possible conditions.

Below are key methods for defining formal specifications, with code examples in CVL:

Product Stories

Derived from user requirements and real-world usage scenarios.

Example: “User balance should always increase by the deposit amount after a successful deposit.”

rule depositIncreasesBalance(uint256 amount) {
     env e;     require(amount > 0);
     uint256 balanceBefore = balanceOf(e.msg.sender);
     deposit(amount);
     uint256 balanceAfter = balanceOf(e.msg.sender);
     assert(balanceAfter == balanceBefore + amount, "Balance did not increase correctly after deposit");
}

When writing formal verification rules, it’s helpful to follow this general structure:

1. Preconditions: Use require statements to set up the initial state and constraints.
2. Function Call: Execute the smart contract function being verified.
3. Postconditions: Use assert statements to check that the desired properties hold after the function executes.

This structure helps in clearly defining what conditions should be true before and after a function’s execution, making specifications more readable and maintainable.

Note: In CVL (Certora Verification Language), require and assert statements behave differently from their Solidity counterparts:

• A require statement that isn't met doesn't halt execution; instead, it filters out scenarios that don't meet the precondition.
• An assert a statement that isn't met results in a violation message and a backtrace, indicating a potential issue in the contract logic.

System Invariants

Invariants are properties that must always hold true throughout the system’s lifecycle.

Example: “The total supply of tokens remains constant unless explicitly minted or burned.”

invariant totalSupplyEqualsSumOfBalances() {
     totalSupply() == sum(address a in accounts, balanceOf(a));
}

Security Properties

These rules ensure that only authorized users can perform specific actions.

Example: “Only the contract owner can perform administrative actions.”

rule onlyOwnerCanPerformAdminActions() {
     env e;
     require(e.msg.sender != owner());
     performAdminAction@withrevert(e);
     assert(lastReverted, "Non-owner was able to perform an admin action"); 
}

This rule uses two important CVL-specific constructs:

• @withrevert operator indicates the function call might revert. The rule attempts to perform an admin action with a non-owner caller, allowing for the possibility of reversion.
• lastReverted keyword returns true if the previous operation reverted. The rule asserts that the action indeed reverted, confirming that non-owners cannot perform it.

This approach leverages CVL’s features to verify security properties by attempting potentially invalid operations and ensuring they fail as expected.

Protocol Behavior

Understanding the expected behavior of a protocol ensures that core functions operate correctly.

Example: “A user’s balance should decrease by the withdrawal amount.”

rule withdrawalDecreasesBalance(uint256 amount) {
     env e;
     require(amount > 0);
     uint256 balanceBefore = balanceOf(e.msg.sender);
     withdraw(amount);
     uint256 balanceAfter = balanceOf(e.msg.sender);
     assert(balanceAfter == balanceBefore - amount, "Balance did not decrease correctly after withdrawal"); 
}

General Guidelines for Rule Creation

Beyond these specific types, there are general guidelines for creating effective verification rules. These guidelines often derive from the nature of the system state or behavior being checked:

• Additivity: Verify that the sum of components equals the whole. For example, check if the total supply of tokens always matches the sum of all account balances.
• Monotonicity: Confirm that certain values change in only one direction under specific conditions. For instance, ensure a liquidity pool’s total value locked (TVL) only decreases during withdrawals and only increases during deposits.
• Bounds checking: Set and verify acceptable ranges for critical values. For instance, confirm that a token’s transfer amount never exceeds the sender’s balance.
• Composability: Ensure interactions between different protocols or contract modules don’t lead to unexpected states. For example, verify that a flash loan taken from one protocol doesn’t leave another integrated protocol in an inconsistent state after the transaction completes.
• Atomicity: Verify that multi-step operations either complete fully or revert entirely. For instance, ensure that in a token swap, either both token transfers occur or neither does.

By incorporating these principles, you can create a more comprehensive set of verification rules that cover complex interactions and edge cases in your smart contracts.

Symbolic Variables

In formal verification, symbolic variables represent entire ranges of possible values, allowing the verification system to evaluate whether rules hold for all potential states of the system.

For instance, when verifying a deposit() function, we might use a symbolic variable for the deposit amount. This single variable doesn’t represent just one specific amount, but rather any possible uint256 value greater than zero. The verification system can then reason about the behavior of the function for all valid deposit amounts simultaneously.

Similarly, we might treat the sender address as a symbolic variable, representing any valid Ethereum address. This allows the verification process to consider all possible user interactions with our contract.

This approach enables formal verification tools to:

1. Consider all possible inputs without explicitly testing each one.
2. Prove properties that hold for entire classes of inputs.
3. Discover edge cases that might be missed by traditional testing with concrete values.

In our upcoming practical example, we’ll see how these symbolic variables are used in formal specifications and how they enable comprehensive verification of smart contract behavior.

Practical Example: From Code to Proofs

Let’s consider a basic Vault contract where users can deposit and withdraw Ether:

contract Vault {
    mapping(address => uint256) public balances;
    function deposit() external payable {
        require(msg.value > 0, "Deposit must be greater than zero");
        balances[msg.sender] += msg.value;
    }

    function withdraw(uint256 amount) external {
        require(amount > 0, "Withdrawal amount must be greater than zero");
        require(amount <= balances[msg.sender], "Insufficient balance");
        balances[msg.sender] -= amount;
        payable(msg.sender).transfer(amount);
    }
}

Step 1: Defining Formal Specifications

We want to verify that a withdrawal always decreases the user’s balance by the exact amount withdrawn:

rule withdrawalDecreaseBalance(uint256 amount) {
    env e;
    require(amount > 0);
    require(amount <= balances[e.msg.sender]);
    
    uint256 balanceBefore = balances[e.msg.sender];
    withdraw(amount);
    uint256 balanceAfter = balances[e.msg.sender];
    
    assert(balanceAfter == balanceBefore - amount, "Balance not decreased correctly");
}

Step 2: Translating to Logical Formulas

The verification tool translates our specifications and relevant contract codes into logical formulas. These directly correspond to the components of our rule:

• Let A represent: amount > 0
• Let B represent: amount <= balances[e.msg.sender]
• Let C represent: balanceAfter == balanceBefore — amount

Step 3: Constructing the SAT Formula

These logical formulas are combined into a Boolean SAT (satisfiability) formula:

(A ∧ B) → C

In propositional logic, this translates to:

¬A ∨ ¬B ∨ C

Where: ¬ means not, ∨ means or, ∧ means and (though not used in this specific formula). This notation, known as a clause in Conjunctive Normal Form (CNF), is a standard format that SMT solvers use to process logical statements efficiently.

Therefore, the above formula simply reads: “Either the amount is not valid (¬A ∨ ¬B), or the balance is correctly decreased after withdrawal C”

We use the negation of the original formula because we’re employing a proof-by-contradiction approach. We’re asking the SMT solver to find a case where our assertion doesn’t hold. Therefore, the SMT solver searches for counterexamples to disprove our assertion. If no such is found, the system is proven correct.

Step 4: SMT Solving

The SAT formula ¬A ∨ ¬B ∨ C is passed to an SMT (Satisfiability Modulo Theories) solver. SMT solvers are powerful tools that determine whether a logical formula can be satisfied under certain constraints. Some popular SMT solvers include:

• Z3: Developed by Microsoft Research, widely used in formal verification
• CVC4: Developed by Stanford University, NYU, and the University of Iowa
• Yices: Developed by SRI InternationalZ3: Developed by Microsoft Research, widely used in formal verification

These solvers use sophisticated algorithms and heuristics to efficiently search the solution space, considering various strategies to quickly find potential violations or prove that no violations exist.

In our case, the SMT solver attempts to find an assignment that makes the SAT formula false, which would indicate a violation of our specified behavior.

Step 5: SMT Solver Results

The SMT solver tries to find an assignment of boolean values to our logical variables A, B, and C that makes the formula ¬A ∨ ¬B ∨ C false.

The reason we look at the negation is rooted in how we’re using formal verification to prove correctness. We’re trying to prove that our original formula (A ∧ B) → C always holds true. In other words, we’re asserting that there are no cases where A and B are true, but C is false.

To prove this, we use a proof-by-contradiction approach:

1. We assume there might be a case where our assertion doesn’t hold.
2. This case would be represented by A ∧ B ∧ ¬C (our preconditions are met, but our postcondition isn’t).
3. We ask the SMT solver to find such a case.
4. If the solver can’t find any such case, we’ve proved our original assertion.

The SMT proceeds to find an assignment that makes A ∧ B ∧ ¬C true. Let’s say it finds that assignment A = true, B = true, C = falsefalsifies the formula, indicating a potential violation of our specified behavior.

Step 6: Backtracking to a Counterexample

Now we need to interpret this abstract result in terms of our original specification and code. Here’s how we backtrack:

1. A = true means amount > 0
2. B = true means amount <= balances[e.msg.sender]
3. C = false means balanceAfter != balanceBefore — amount

This process of deriving concrete values from the abstract assignment is known as counterexample generation. It’s typically performed by the verification tool in conjunction with the SMT solver, using the theories understood by the solver (like integer arithmetic) to find specific values that satisfy the abstract conditions.

The SMT solver finds one possible set of values:

• amount = 100
• before withdraw: balances[e.msg.sender] = 100
• after withdraw: balances[e.msg.sender] = 1

This counterexample satisfies A and B (as they’re both true), and violates C (as it’s false).

Step 7: Tracing Back to Code

Interpreting this counterexample, we can see that our contract fails to correctly update the balance when a user withdraws their entire balance. The balance is decreased, but not by the exact amount withdrawn.

Step 8: Fixing and Re-verifying

To fix this issue, we need to ensure that the balance is decreased by exactly the withdrawal amount:

function withdraw(uint256 amount) external {
    require(amount > 0, "Withdrawal amount must be greater than zero");
    require(amount <= balances[msg.sender], "Insufficient balance");
    balances[msg.sender] -= amount;  // This line ensures the balance is decreased by exactly 'amount'
    payable(msg.sender).transfer(amount);
}

After making this change, we would run our formal verification again. If the SMT solver can’t find any assignment that falsifies our formula, we have mathematically proven that our withdrawal function correctly updates the balance for all possible valid inputs.

Verification Process Summary

This process — from code to logical formulas to SMT solving, and back to concrete scenarios — allows us to verify the correctness of our smart contracts with a level of certainty far beyond what traditional testing can provide:

By considering all possible states and transitions, formal verification helps us catch subtle bugs and edge cases that might otherwise go unnoticed, providing a powerful tool in our quest for secure and reliable smart contracts.

Certora Prover: Comprehensive Formal Verification

While we’ve explored how SMT solvers work in formal verification, let’s now explore a powerful tool that automates, streamlines, and enhances this process. Certora Prover, developed by a team of leading Ph.D. researchers in the field, is a scientific-heavy tool that pushes the boundaries of formal verification for smart contracts.

Certora Prover offers a wide range of features to enhance the verification process:

• Expressive Specification Language (CVL): Allows precise property definitions tailored for smart contracts.
• Automated Verification: Converts specifications and bytecode into SMT problems.
• Bytecode-Level Analysis: Provides more accurate and trustworthy verification results compared to source code analysis alone, as it accounts for any changes or optimizations introduced during the compilation process.
• Parameterized Systems: Allows verification of contracts that interact with other contracts, considering various possible implementations.
• Prover Debugger: Helps developers understand and debug the verification process itself.
• Rule-Code Coverage: Helps developers understand which parts of their code are covered by the verification rules, ensuring comprehensive testing.
• Mutation Testing: Automatically introduces small changes in the code to test the robustness of the verification rules.
• Detailed Feedback: Provides counterexamples for debugging when violations are found.
• Integration Capabilities: Works seamlessly with development tools and CI/CD pipeline.

The Challenges of Formal Verification

It’s important to note that formal verification is only as good as the specifications it tests against. If the specs don’t capture all edge cases or reflect intended behavior correctly, the verified code might still have problems. As they say, “Garbage in, garbage out.”

Computationally, the process of iterating through all possible states of a system is an incredibly complex problem. To put it simply, the number of possible states grows beyond exponentially with the complexity of the system. In computer science terms, this is known as an NP-hard problem or, in some cases, even an undecidable problem.

Because of this inherent complexity, a significant amount of scientific research goes into developing efficient heuristics. These heuristics aim to reduce the problem space by efficiently pruning irrelevant execution paths.

The goal is to minimize what is called “timeouts” — instances where the verification process exceeds a predefined time limit and is automatically terminated.

Despite these challenges, tools like Certora Prover have made significant strides in making formal verification practical for complex smart contracts.

Applicability of Formal Verification in Smart Contracts

Formal verification is particularly well-suited for smart contract verification due to several factors:

1. Single-threaded Execution: Smart contracts typically execute in a single-threaded environment, simplifying the verification process.
2. Relatively Short Code: Most smart contracts are concise, making them more manageable for exhaustive verification.
3. High-stakes Operations: With millions of dollars at stake, the cost of formal verification is justified by the potential losses it can prevent.
4. Immutability: Once deployed, smart contracts can’t be easily updated, making it crucial to verify correctness before deployment.

These characteristics make formal verification a powerful tool for enhancing smart contract security and reliability, especially for high-value DeFi protocols.

The Interconnected Nature of Security Measures

While formal verification is powerful, it’s most effective when used as part of a comprehensive security strategy. The most robust approach involves:

1. Continuous Verification: Every proposed change (e.g. pull requests submitted as a part of governance in AAVE protocol), including those through governance, should pass through a comprehensive security process, including formal verification, manual audits, automated analysis, and economic simulations.
2. Manual Audits: Expert reviewers manually inspect the code to identify issues that automated tools might miss, especially those related to business logic or novel attack vectors.
3. Real-Time Monitoring: Tools like Hypernative offer continuous blockchain state monitoring, which adds an additional layer of security to complement formal verification. These tools analyze transactions and system state changes in real-time, potentially catching harmful transactions and method calls before execution.

The Importance of Reputable Verification

Not all security audits are created equal. As users and investors in the DeFi space, it’s essential to evaluate the security measures of protocols you interact with. When assessing a protocol’s security:

Look for Reputable Verifiers: Seek out protocols that have been verified by well-respected firms known for their rigorous processes.

1. Multiple Audits: Protocols that have undergone multiple audits from different reputable firms often demonstrate a stronger commitment to security.
2. Ongoing Verification: Look for protocols that employ continuous verification processes, not just one-time audits.
3. Transparency: Check if the protocol makes its audit reports and verification results publicly available.

For a comprehensive history of smart contract exploits, resources like DeFi Llama’s “Rekt Database” (https://defillama.com/hacks) provide valuable insights into past vulnerabilities and their impacts.

Conclusion

The security of smart contracts and DeFi protocols presents a multi-faceted challenge that demands a comprehensive approach. By combining formal verification, rigorous manual auditing, continuous monitoring, and real-time analysis, we can create a robust security ecosystem. However, it’s important to understand that no single method, including formal verification, is perfect. The exponential complexity of verifying all possible states means that even the most advanced tools have limitations.

For users and investors in the DeFi space, understanding these security measures is crucial. Always look for protocols that employ a diverse range of reputable security measures and maintain transparency about their security processes. Remember, a protocol that undergoes continuous verification, including for all governance-proposed changes, demonstrates a stronger commitment to security than one that allows unaudited modifications.

As the field of formal verification continues to advance, driven by cutting-edge research and practical applications in high-stakes environments like DeFi, we can expect even more sophisticated tools and methodologies to emerge. This ongoing evolution of security practices will play a vital role in building a more secure and trustworthy decentralized future.

Resources

For readers interested in deepening their understanding of formal verification and the Certora Prover, here is a curated list of valuable resources I’ve found particularly helpful:

• The comprehensive CVL tutorial with explanations: https://docs.certora.com/projects/tutorials/en/latest/
• Code-based tutorial with a set of runnable examples: https://github.com/Certora/Tutorials/
• A nice introduction to Certora Prover: https://www.youtube.com/watch?v=jv_1hEeG-lk&t=1849s&ab_channel=Certora%E2%80%8B by Mike George from Certora
• Certora Prover walkthrough: https://www.youtube.com/watch?v=c5ViO3Dpfqs&ab_channel=Certora%E2%80%8B by Chandrakana Nandi from Certora
• Checking formal specifications workshop: https://www.youtube.com/watch?v=PjUua2Hi1GA&t=1568s&ab_channel=Certora%E2%80%8B by Nurit Dor from Certora
• Certora Discord is the best place to get help on every question along the road from onboarding to heavy usage: https://discord.gg/certora (with special thanks to Aleksander for his patience in answering all my questions and for reviewing this article)

Find me on LinkedIn, Telegram, X (a.k.a. Twitter), Farcast.