Formal verification in DeFi: what a proof buys you

Testing shows that code behaves correctly on the inputs that were tried. Formal verification aims to show that it behaves correctly on all of them. For contracts that hold other people’s money and cannot easily be changed once deployed, that difference is attractive, and formal methods are now a routine part of reviewing the most critical DeFi code.

A proof is also easy to over-read. It establishes that a specific property holds for a specific model of the code under specific assumptions. Each of those qualifiers can hide the bug that matters. This analysis maps the main techniques, what each one establishes, and the questions a reader should ask of any verification result.

What a proof promises

Every verification result has three ingredients. A specification states what must be true, such as “total shares never exceed total assets” or “only the owner can pause.” A model describes what the code can do, derived from source or bytecode together with the semantics of the virtual machine. A tool searches for a way the model can violate the specification. If it finds none, within the limits it was given, the property is proved for that model.

The guarantee is therefore conditional. It says nothing about properties that were not written down, and it is only as faithful to the deployed contract as the model is.

Four techniques, four strengths

The techniques are complementary. Symbolic tests are cheap to adopt because they look like unit tests. Rule-based provers can reason about every reachable state rather than one starting point, at the cost of more specification work. Equivalence checking is the right tool for a narrow but important question, such as whether a gas optimisation or a recompilation changed behaviour.

The boundary of a proof

Three outcomes are possible. A proof holds for the model as specified. A counterexample is a concrete trace that violates the property, and is often the most valuable output because it can be replayed as a test. A timeout means the tool gave up, and it is not evidence either way. Reports that list only proved properties without the timeouts are incomplete.

Writing properties worth proving

The hardest part of formal verification is deciding what to prove. Good properties come from the protocol’s promises to its users, stated as precisely as possible. The symbolic test below checks a simple but meaningful one: a deposit followed by a redemption cannot create value.

1// Illustrative symbolic test for halmos: functions prefixed check_ are explored2// with symbolic arguments, covering every value in the assumed range at once.3contract VaultRoundTripTest is Test {4    Vault vault;5 6    function setUp() public {7        vault = new Vault(new TestToken());   // the proof is about this starting state8    }9 10    /// Depositing and immediately redeeming never returns more than was deposited.11    function check_noValueCreatedOnRoundTrip(uint256 assets) public {12        vm.assume(assets > 0 && assets < 1e30);13        uint256 shares = vault.deposit(assets, address(this));14        uint256 back   = vault.redeem(shares, address(this), address(this));15        assert(back <= assets);16    }17}

The test explores every value of assets in the assumed range at once. It does so from one starting state, the one setUp creates, so it proves nothing about a vault that already holds deposits from others. That is a typical limit of symbolic testing and the reason rule-based provers reason about invariants that must hold in every reachable state.

1// Illustrative rule in the Certora Verification Language (CVL).2methods {3    function balanceOf(address) external returns (uint256) envfree;4}5 6/// A withdrawal by one account never changes another account's balance.7rule withdrawIsolated(address other) {8    env e;9    uint256 amount;10    require other != e.msg.sender;11 12    mathint before = balanceOf(other);13    withdraw(e, amount);14    assert balanceOf(other) == before, "withdraw touched a third party";15}

The rule states an isolation property: one account’s withdrawal never changes another account’s balance. Because it is checked from an arbitrary state, it covers vaults with any history. Properties of this kind, about who can affect whom, catch access-control and accounting bugs that are hard to anticipate as individual test cases. The primer on writing invariants covers how to derive such properties from requirements.

Assumptions that decide the result

Every model simplifies. The simplifications that most often matter in DeFi are these:

• External calls. Calls to tokens, oracles and other protocols are usually replaced by summaries: a function that returns any value, or a fixed one. A summary that is more polite than the real contract, for instance one that never re-enters, hides the bugs the real contract would expose.
• Bounds. Loops are unrolled a fixed number of times, arrays are limited in length, and call depth is capped. Bugs that appear only beyond those bounds are not found.
• Environment. Assumptions about msg.sender, timestamps, token decimals and initial state narrow the space explored. Each one is a statement that the property is only claimed under that condition.
• What is deployed. Compiler version and settings, constructor arguments, proxy configuration and later upgrades are outside the proof unless verified separately.

Where proofs pay off in DeFi

Formal methods earn their cost where a property is easy to state, hard to test exhaustively, and catastrophic to violate. In DeFi that typically means solvency and accounting invariants (assets cover liabilities, the sum of balances equals total supply), access control (which functions can change which state, and who can call them), monotonicity (an index or exchange rate that must never decrease), and upgrade safety (the new implementation behaves like the old one except where intended).

Proofs pay off less where the risk is economic rather than logical. A lending market can be proved to liquidate exactly as specified and still be drained by an oracle whose price was manipulated, because the price is an input the proof treats as given. That boundary is why formal verification complements, rather than replaces, economic review and adversarial testing.

Reading a verification report

When a protocol advertises formal verification, these questions determine what it actually means:

1. Which properties were specified, and do they cover the protocol’s promises to users?
2. Which contracts and functions were in scope, and which external calls were summarised, and how?
3. What bounds were used for loops, arrays and call depth?
4. Which properties timed out or were not proved, and what was done about them?
5. Were vacuity or sanity checks run on every rule?
6. Does the verified code match the deployed bytecode and configuration?

The Fenwick Lending research assessment shows how properties and their assumptions are recorded alongside manual findings, and the formal verification service describes the engagement structure.

Conclusions

A formal proof is the strongest evidence available that a property holds, and it is strictly limited to the property, the model and the assumptions. The most consequential choices in a verification effort are therefore not about tools but about which properties to write, how external behaviour is summarised, and what bounds are accepted.

Used with that discipline, formal methods find bugs that no test suite would. Used as a badge, they can produce confidence the evidence does not support.

Recommendations