Formally Verifying the World's Most Popular Smart Contract

Abstract

Wrapped ETH, or WETH↗, is one of Ethereum’s most popular smart contracts. While WETH serves a simple purpose, a significant portion of all Ethereum transactions depend on it. WETH now underpins large parts of DeFi. In this blog post, we prove critical safety guarantees and invariants within the WETH contract. We do so by leveraging Z3, a battle-tested SMT solver.

We prove two critical invariants: (1) correctness of accounting, and (2) solvency. For accounting, we prove that the total supply of WETH is always equal to its balance of native Ether. For solvency, we prove that, regardless of other users’ actions, a user is always able to unstake Wrapped ETH. In the process, we also identified a minor, harmless bug in the contract. Our work enables the community to continue using WETH with increased confidence in its correctness.

Background

WETH is a straightforward token that wraps native Ether into the ERC20-compatible WETH token. The contract allows anyone to deposit native Ether for WETH tokens 1:1, or conversely, redeem WETH for native Ether. The contract also supports the standard ERC20 functionality, like approvals, transfers, totalSupply, and transferFrom.

WETH is useful because native Ether is inconvenient for use in smart contracts. First, native Ether is not ERC20 compatible. This necessitates additional code paths, increasing complexity. Not only does this add developmental burdens, it increases the likelihood for security vulnerabilities. Native Ether interactions also introduce the risk of re-entrancy vulnerabilities, which are absent when dealing with ERC20 tokens. Hence, WETH has seen widespread adoption in DeFi applications, like Uniswap, Compound, etc.

As of the time of writing, WETH has been involved in over 125 million transactions¹. On the entire Ethereum blockchain, there have been 1.7 billion transactions so far. In other words, over 7% of all Ethereum transactions involve Wrapped ETH. Furthermore, Wrapped ETH has become more pervasive over time. In the past year, 48M of 420M Ethereum transactions called WETH. This represents 11.5% of all Ethereum transactions this year. Since WETH is heavily used in DeFi applications, and DeFi has become a centerpiece of the Web3 ecosystem, this is a natural outcome.

A smart contract bug in WETH would be deadly. Countless DeFi protocols use WETH as as a compatibility layer for native ETH. For instance, Uniswap relies on WETH↗ internally when dealing with native ETH. Should WETH have a solvency or accounting error, the downstream effects on DeFi would be massive. Not only would WETH holders be affected, so would all of the DeFi protocols which are hardcoded to use WETH internally.

The WETH contract itself is relatively simple. Excluding blank lines and comments, WETH9 is comprised of only 51 lines of code in total. Excluding getters, there are only 7 functions, and each of these functions are relatively simple. That being said, simplicity is no guarantee of correctness. In fact, the first ever known instance of a reentrancy attack was performed on a WETH-style wrapper contract↗. Incidents like this reveal the importance of formal verification of critical smart contracts.

That being said, let’s quickly review the most important functions in WETH:

• balanceOf: A mapping from addresses to uint256 that tracks how much WETH a given address “owns”.
• deposit: Payable function. Accepts native ETH in msg.value and mints new WETH to msg.sender by adding to their account entry in balanceOf.
• withdraw: Function. Burns WETH by subtracting from the sender’s entry in balanceOf, and disburses an equal amount of native ETH.
• totalSupply: View function. Computes the total amount of outstanding WETH issued by taking the native ETH balance of the WETH contract itself.
• transferFrom: Function. Transfers WETH tokens among different accounts. It also enforces ERC20 token allowance rules, blocking unauthorized transfers.

As we verify the correctness of WETH, we will need to keep each of these functions in mind.

Methods

Using Z3Py, we reimplemented the WETH contract behavior in SMT equations. We then used the Z3 theorem prover to prove certain facts about the symbolized WETH contract. First, we proved a key invariant concerning the correctness of WETH’s internal accounting. Second, we proved an invariant guaranteeing that WETH holders can always withdraw their locked ETH.

Invariant 1: Internal accounting correctness

A key invariant of WETH is that totalSupply must equal the sum of all entries in balanceOf. In other words, WETH must correctly track its total supply. This is reinforced in the ERC-20 standard. According to EIP-20, a token’s totalSupply function must “return the total token supply”. It seems important for a widely-used contract like WETH to obey the ERC20 token standard.

The WETH contract computes totalSupply by simply using address(this).balance, which returns the native ETH stored in the contract total. This amount should match up with the total supply of WETH ERC20 token, since balanceOf and native ETH are always added and subtracted commensurately, simultaneously (in the functions deposit and withdraw, respectively).

Interestingly, while I was formally verifying this property, I discovered that this invariant doesn’t actually hold↗. It’s possible to cause WETH to return a totalSupply that’s unequal to the total number of WETH tokens. So technically, WETH’s totalSupply function is wrong! But we’ll see later why that doesn’t really matter.

Let’s first begin by formalizing the various properties of WETH that have to do with this invariant. First, the invariant only depends on totalSupply, balanceOf, and the contract’s native ETH balance. For the purposes of this invariant, we can summarize the relevant global state in a 2-tuple: $(balanceO\mkern-3mu f, weth\_balance)$. Here, $balanceO\mkern-3mu f$ is a mapping from address to uint256, and $weth\_balance$ is a uint256.

Next, because the WETH contract may not operate properly under conditions where there is an infinite supply of native ETH in circulation, we augment our state tuple with a third variable, $eth\_supply$: uint256 which represents (overapproximates) the total supply of native ETH outside of our WETH contract (in wei). The new variable, $eth\_supply$ will constrain any native ETH values in transactions. Thus, our state tuple is $(balance\mkern-3mu Of, weth\_balance, eth\_supply)$.

Since the invariant is fully parameterized by our state tuple, we need only consider the ways the components of the state tuple can be affected. Enumerating them, we have:

• deposit, fallback, and withdraw: updates $balanceO\mkern-3mu f$ and the native ETH balance
• transferFrom: updates $balance\mkern-3mu Of$
• SELFDESTRUCT or block reward coinbase↗: updates the native ETH balance (applies to any address, not just WETH)

We can formalize each of these state transitions as a guarded transition rule. Each rule takes the form $(state, parameters) \bigm\lvert condition \longrightarrow new\_state$, where $state$ and $new\_state$ are state tuples, $parameters$ is a tuple of arguments for the transition, and $condition$ is a predicate required for the transition to be valid. We have the following rules:

• deposit: $((balanceO\mkern-3mu f, weth\_balance, eth\_supply), (msg\_sender, msg\_value))$ $\bigm\lvert msg\_value \leq eth\_supply$ $\longrightarrow (\text{Store}(balanceO\mkern-3mu f, src, balanceO\mkern-3mu f[src] + msg\_value), weth\_balance + msg\_value, eth\_supply - msg\_value)$

• withdraw: $((balanceO\mkern-3mu f, weth\_balance, eth\_supply), (msg\_sender, wad))$ $\bigm\lvert wad \leq balanceO\mkern-3mu f[msg\_sender]$ $\longrightarrow (Store(balanceO\mkern-3mu f, msg\_sender, balanceO\mkern-3mu f[msg\_sender] - wad), weth\_balance - wad, eth\_supply + wad)$

• transferFrom: $((balanceO\mkern-3mu f, weth\_balance, eth\_supply), (src, dst, wad))$ $\bigm\lvert wad \leq balanceO\mkern-3mu f[src]$ $\longrightarrow (Store(x, dst, x[dst] + wad), weth\_balance), where x = Store(balanceO\mkern-3mu f, src, balanceO\mkern-3mu f[src] - wad, eth\_supply)$

• selfdestruct: $((balanceO\mkern-3mu f, weth\_balance, eth\_supply), (value))$ $\bigm\lvert msg\_value \leq eth\_supply$ $\longrightarrow (balanceO\mkern-3mu f, weth\_balance + value, eth\_supply - value)$

• fallback: same as deposit

• coinbase: essentially same as fallback (overapproximation)

where $Store(M, K, V)$ denotes a mapping identical to $M$ but with $M[A]$ set to $V$.

We’ll also define an initial state for the contract:

• $(K(0), 0, 120000000e18)$, where $K(0)$ denotes the mapping with all entries initialized to 0.

We choose 120000000e18 as the concrete value for $eth\_supply$ here, as there are roughly 120M ether in circulation. Since a large portion of the total eth supply is locked up elsewhere already, this is a sound overapproximation.

Constrained Horn Clauses

Since our invariant is an inductive property, it’s tricky for a SMT solver like Z3 to prove directly. We’ll solve this by formulating the contract’s semantics as Constrained Horn Clauses↗, or CHC for short [1]↗ [2]↗ [3]↗. Conveniently, Z3 features a relatively robust CHC engine. CHC is also used by solc’s SMTchecker↗. However, I could not get the CHC engine built into SMTchecker to work for our purposes. This is likely due to limitations in the Z3 solver, which we explore later in the article. Instead, we used Z3 directly with our own hand-written CHCs.

Although there is already a decent amount of literature surrounding Constrained Horn Clauses, for the sake of accessibility, we’ll walk through a brief introduction of them in this section. We’ll also go through a few examples at each step to keep things friendly.

First, we define a function, $\text{State}(s)$, which is true iff $s$ is a valid state tuple that can be reached from a starting state using our predefined set of state transition rules. In other words, $\text{State}(s)$ enumerates all of the possible states our smart contract could get to.

For instance, $State(K(0), 0, 0)$ should be False, because it’s impossible for all of the outstanding ETH supply to disappear; it either has to go into the WETH contract or it either stays circulating. More formally, you could say, that given some $s = (balanceO\mkern-3mu f, weth\_balance, eth\_supply)$, then $\text{State}(balanceO\mkern-3mu f, weth\_balance, eth\_supply)$ necessarily implies that $weth\_balance + eth\_supply$ is always equal to some constant. While doing our formal verification, we’d like to assume as few things as possible beyond our predefined state transitions and initial states. To prove this property, we could add this implication in the SMT solver as an additional assertion.

Keep in mind that our goal here is to verify that the sum of all entries in $balanceO\mkern-3mu f$ (the real total supply) equals to $weth\_balance$ (the computed total supply). We would formulate this invariant as a CHC assertion that:

$\forall s = (balanceO\mkern-3mu f, weth\_balance, eth\_supply) : \text{State}(balanceO\mkern-3mu f, weth\_balance, eth\_supply) \implies \sum_{a} balanceO\mkern-3mu f[a] = weth\_balance$

If it’s possible to reach a state where the constraint does not hold, then our implication assertion will be violated. As a result, the SMT solver will report that our constraints are unsatisfiable. In other words, the solver is reporting that it’s impossible to synthesize a function $\text{State}$ such that it obeys both our state transition (i.e., reachability) rules as well as the additional constraints we’re aiming to prove. Furthermore, we can query the prover for an unsatisfiability proof, which provides us a logical sequence from our starting set of assertions to a violating state. This sequence is often a path from our initial state, through a series of state transitions, to an illegal state. This is helpful for debugging why our assumptions or invariants are invalid.

On the other hand, if our invariants hold in all reachable states, then our assertions will hold. The SMT solver will report that the system is satisfiable. In other words, it’s possible to synthesize the function $\text{State}$ consistent with both our state transition rules and our invariants. It also means our invariants are consistent with the state transition rules. In that case, we can query the solver for a model, which will actually have a concrete definition for a possible synthesization of $\text{State}$. This definition will essentially be a predicate outlining all reachable states.

CHC formulation of WETH’s state transition rules

We start by asserting a set of valid initial “starting” states and transition rules constraining $\text{State}(s)$. For WETH, this is essentially the contract state after the constructor returns.

$\text{State}(K(0), 0, 120000000e18) = \text{True}$

Then, for each transition rule, we formulate it as a CHC, and assert it. More concretely, each of our formulae will take a form like:

$\forall (s, p) : (\text{State}(s) \land \text{Pre}(p)) \implies \text{State}(\text{Post}(s, p))$

where $s$ is a state tuple, $p$ is a parameters tuple, $\text{Pre}(p)$ is a boolean function that represents the preconditions that the parameters $p$ are checked against, and $\text{Post}(s, p)$ represents the updated state after the transition. Intuitively, this means: “for each state $s$ and parameter vector $p$, if $s$ is a reachable state, and $p$ are valid parameters, then we can also reach the updated state $\text{Post}(s, p)$“.

For example, here is our formula for the withdraw transition:

$\forall (balanceO\mkern-3mu f, weth\_balance, msg\_sender, wad) : (\text{State}(balanceO\mkern-3mu f, weth\_balance, eth\_supply \land (wad \leq balanceO\mkern-3mu f[msg\_sender]) \land (weth\_balance \leq wad)) \implies \text{State}(\text{Store}(balanceO\mkern-3mu f, msg\_sender, balanceO\mkern-3mu f[msg\_sender] - wad), weth\_balance - wad, eth\_supply + wad).$

Here, the preconditions check that the user has sufficient WETH balance (enforced in the smart contract), and that the WETH contract has sufficient native ETH to send (enforced in the EVM). The updated state is identical to the input state, except the user’s balance has been updated, the WETH contract has less native ETH, and the user has more native ETH.

Encoding sums over arrays

The invariant that we wish to check is that the sum of all values in $balanceO\mkern-3mu f$ is equal to $weth\_balance$; i.e., $\sum balanceO\mkern-3mu f = weth\_balance$. Encoding this sum in SMT is difficult, as there is no natural way to express the sum within the standard SMT Array theories↗.

To resolve this, we introduce an additional “synthetic” variable, $sum\_balanceO\mkern-3mu f$ that tracks the value of this sum; i.e., $sum\_balanceO\mkern-3mu f := \sum balanceO\mkern-3mu f$. We augment the state tuple with this additional synthetic variable. This trick is correct as long as we accordingly update $sum\_balanceO\mkern-3mu f$ wherever $balanceO\mkern-3mu f$ is updated. For example, when adding or subtracting to any elements of $balanceO\mkern-3mu f$, we will correspondingly add or subtract to $sum\_balanceO\mkern-3mu f$.

As a CHC, our invariant can be formulated as such:

$\forall (balanceO\mkern-3mu f, weth\_balance, msg\_sender, wad, sum\_totalSupply) : (\text{State}(balanceO\mkern-3mu f, weth\_balance, eth\_supply, sum\_totalSupply)) \implies sum\_totalSupply = weth\_balance$

However, this fix alone is not sufficient in “strengthening” Z3’s Arrays theory implementation enough to prove our constraint systems in a timely fashion. As an implementation detail, since Z3 does not “understand” that $sum\_balanceO\mkern-3mu f$ is a sum over $balanceO\mkern-3mu f$, it is unable to easily prove global properties about the values in $balanceO\mkern-3mu f$. If forced, it will generally resort to brute force proofs enumerating all possible addresses. Clearly, this is not feasible for Ethereum (addresses are 160-bit). Thus, we also augment all transition rules with the additional precondition that $balanceO\mkern-3mu f[x] \leq sum\_balanceO\mkern-3mu f$, when the transition uses some value $balanceO\mkern-3mu f[x]$. This approximation is sound, because by definition, $sum\_balanceO\mkern-3mu f$ is a sum over all values in $balanceO\mkern-3mu f$, and a sum is always greater than or equal to an individual component. Most importantly, these additional constraints enable the solver to complete much more quickly. It can easily rule out unreachable states that involve an individual entry greater than our synthetic sum variable.

Furthermore, to help the solver complete more quickly, we “guide” the solver by prompting it to prove an additional lemma. The lemma asserts that both $sum\_balanceO\mkern-3mu f$, as well as all values in $balanceO\mkern-3mu f$ are less than our total eth supply of 120000000e18:

$\forall (balanceO\mkern-3mu f, weth\_balance, msg\_sender, wad, sum\_totalSupply, address) : (\text{State}(balanceO\mkern-3mu f, weth\_balance, eth\_supply, sum\_totalSupply)) \land (balanceO\mkern-3mu f[address] \leq sum\_balanceO\mkern-3mu f) \implies (sum\_balanceO\mkern-3mu f \leq 120000000e18) \land (balanceO\mkern-3mu f[address] \leq 12000000e18)$

In our experiments, we determined that this lemma is necessary to make Z3 avoid brute force proofs.

Results

Surprisingly, when we run our Z3Py code, we immediately discover a counterexample to our invariant:

unsat
mp(hyper-res( # "3"
    asserted(ForAll([A, B, C, D], Implies(
        And(
            state(A, B, C, D),
            Not(D == B)
        ), query!1
    ))),
    hyper-res( # "2"
        asserted(ForAll([A, B, C, D, E, F, G], Implies(
            And(
                state(C, D, E, F),
                B == D + G,
                ULE(G, E),
                A == E + 115792089237316195423570985008687907853269984665640564039457584007913129639935*G # Note: this large constant is 2^256-1
            ),
            state(C, B, A, F)
        ))),
        hyper-res( # "1"
            asserted(state(K(BitVec(160), 0), 0, 120000000000000002281701376, 0)),
            state(K(BitVec(160), 0), 0, 120000000000000002281701376, 0)
        ),
        state(K(BitVec(160), 0), 12884901888, 119999999999999989396799488, 0)
    ),
    query!1
),
asserted(Implies(query!1, False)),
False)

To interpret this, we read it inside-out. In plain English, this is saying:

1. The starting state $(K(BitVec(160), 0), 0, 120000000e18, 0)$ is assumed to be reachable. So therefore, it’s reachable. (Note: this is the hyper-res marked with “1”)
2. You’ve asserted that if a state is reachable, I can also do a SELFDESTRUCT to the WETH contract to reach a new state. Therefore, the state $(K(0), 12884901888, 119999999e18, 0)$ is reachable.
3. You’ve asserted that if a state is reachable, $weth\_balance$ must equal $sum\_balanceO\mkern-3mu f$. But we know that a state where $weth\_balance$ = 12884901888, and $sum\_balanceO\mkern-3mu f$ = 0 is reachable.
4. This is a contradiction, so what you’ve asked me for is logically inconsistent. This isn’t satisfiable.

As we alluded to earlier, this is essentially a bug (albeit minor) in WETH! It’s possible for the totalSupply to not actually be the total number of WETH tokens in existence! And that’s because, as Z3’s proof indicates, that you can SELFDESTRUCT eth into the WETH contract. That increases the eth balance of the contract, but doesn’t mint any new tokens. This desyncs the totalSupply variable! This is a common bug pattern↗ that has been documented before, but it’s surprising for such a popular smart contract to have such a bug. It may be an intended gas optimization, or it could be that the WETH developers found this issue to be insignificant.

In any case, we can still prove a different, but equally valuable invariant about WETH: that the total number of WETH tokens is always less than or equal to the native eth balance of WETH. Note that we’ve relaxed the constraint here to less than or equal constraint, from the originally strictly equals to constraint. Our new CHC invariant formulation would be:

$\forall (balanceO\mkern-3mu f, weth\_balance, msg\_sender, wad, sum\_totalSupply) : (\text{State}(balanceO\mkern-3mu f, weth\_balance, eth\_supply, sum\_totalSupply)) \implies sum\_totalSupply \leq weth\_balance$

Re-running our Z3Py code, we receive our desired sat result!

sat
[state = [else ->
          And(Var(1) == 120000000000000002281701376 + 115792089237316195423570985008687907853269984665640564039457584007913129639935*Var(2),
              ULE(Var(3), Var(1)),
              Extract(255, 87, Var(2)) == 0,
              ULE(154742504910672534362390527*Extract(86, 0, Var(3)) + Extract(86, 0, Var(1)), 120000000000000002281701376),
              Extract(255, 87, Var(1)) == 0
          )
]]

Invariant 2: Solvency

In the previous section, we proved that the total number of WETH tokens is always less than the eth balance of the WETH contract. However, that does not necessarily prove that WETH holders can actually withdraw their eth. In this section, we prove additionally that WETH is solvent, meaning that a WETH holder is always able to withdraw their eth after depositing. In other words, we show that regardless of what happens to the WETH contract in between the deposit and the withdrawal, the depositor is always able to withdraw their eth.

While we can prove this invariant by extending our CHC formulation, that formulation is not very well suited to the line-by-line conditions, statements, and control flow in the WETH contract code. For instance, our CHC formulation simply describes preconditions in state transitions, without any attention paid to the order those preconditions are checked in. This is generally OK since Ethereum transactions are atomic, but it illustrates the general problem that our CHC formulation is a simplification of the full semantics of the WETH contract’s code.

Furthermore, the CHC formulation does not model the approve function or any of the ERC20 allowance functionality in transferFrom. This was previously OK, as we were only interested in proving one specific property of WETH state. However, for a rigorous guarantee of solvency (i.e., ability to withdraw after depositing), we need a more fine-grained approach that more precisely models the semantics of the WETH contract code. More specifically, we will adopt a symbolic execution-based approach.

Symbolic execution of Solidity

The best way to explain our approach is through an example. Let’s take the WETH function approve as an example. Here is the Solidity code for that function:

function approve(address guy, uint wad) public returns (bool) {
    allowance[msg.sender][guy] = wad; // 1
    Approval(msg.sender, guy, wad);   // 2
    return true;                      // 3
}

We translate this Solidity function to a Z3Py function. The function takes, as input, a state tuple like the one described in the previous section. It then symbolically executes each statement. Finally, it returns an updated state tuple. Here is our translated code:

def approve(s, state, msg_sender, guy, wad):
    eth_balances, balanceOf, allowance = state

    # allowance[msg.sender][guy] = wad; (1)
    allowance = Store(allowance, msg_sender, Store(allowance[msg_sender], guy, wad))
    
    # Approval(msg.sender, guy, wad);   (2)
    
    # return true;                      (3)

    return (eth_balances, balanceOf, allowance)

We symbolically execute statement (1) as two symbolic stores. Here, allowance is symbolized as a SMT Array from addresses to Array of addresses to uint256.

We ignore statements (2) and (3), as we are modeling external calls to the WETH contract. Since logs and return values do not affect the WETH state, we don’t care about them. They are essentially side effects that cannot affect WETH’s solvency.

For a more in-depth example, let’s take the deposit function. Here is the Solidity code:

function deposit() public payable {
    balanceOf[msg.sender] += msg.value; // 1
    Deposit(msg.sender, msg.value);     // 2
}

And here is the corresponding symbolic implementation:

def deposit(s, state, msg_sender, msg_value):
    eth_balances, balanceOf, allowance = state

    # transfer of native eth, as per msg_value
    s.add(UGE(eth_balances[msg_sender], msg_value)) # note: UGE means "unsigned greater than"
    eth_balances = Store(eth_balances, msg_sender, eth_balances[msg_sender] - msg_value)
    eth_balances = Store(eth_balances, WETH_Address, eth_balances[WETH_Address] + msg_value)

    # balanceOf[msg.sender] += msg.value; (1)
    balanceOf = Store(balanceOf, msg_sender, balanceOf[msg_sender] + msg_value)
    
    # Deposit(msg.sender, msg.value);     (2)

    return (eth_balances, balanceOf, allowance)

First, since deposit is a payable function, we must model the transfer of native eth into the function in msg_value. We impose the constraint that the sender must have sufficient balance for msg_value. Those three Z3Py statements are implicit from the rules of the EVM.

Next, we symbolically execute line (1), updating balanceOf. Lastly, we can ignore line (2) as it simply emits an event, which we don’t care about.

Finally, let’s look at how we handle branching control flow in the transferFrom function. Here’s the Solidity code:

function transferFrom(address src, address dst, uint wad)
    public
    returns (bool)
{
    require(balanceOf[src] >= wad);                   // (1)

    if (src != msg.sender && allowance[src][msg.sender] != uint(-1)) { // (2)
        require(allowance[src][msg.sender] >= wad);   // (3)
        allowance[src][msg.sender] -= wad;            // (4)
    }

    balanceOf[src] -= wad;                            // (5)
    balanceOf[dst] += wad;                            // (6)

    Transfer(src, dst, wad);

    return true;
}

And here is how we symbolically execute that:

def transferFrom(s, state, msg_sender, src, dst, wad):
    eth_balances, balanceOf, allowance = state

    # (1)
    s.add(UGE(balanceOf[src], wad))

    # (2)
    p = And(src != msg_sender, allowance[src][msg_sender] != Uint(0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff))
    
    # (3)
    s.add(Implies(p, UGE(allowance[src][msg_sender], wad)))
    
    # (4)
    allowance = If(p,
        Store(allowance, src, Store(allowance[src], msg_sender, allowance[src][msg_sender] - wad)),
        allowance)
    
    # (5)
    balanceOf = Store(balanceOf, src, balanceOf[src]-wad)
    
    # (6)
    balanceOf = Store(balanceOf, dst, balanceOf[dst]+wad)

    return (eth_balances, balanceOf, allowance)

When we symbolically execute code in this style, we effectively must symbolize the values of variables on both paths of all branches. In statement (4), allowance receives either an updated value if the branch is taken (p is true) and otherwise remains unchanged (p is false).

It should be noted that in the presence of loops, this style of symbolic execution can lead to what is known as the path explosion problem↗, where each loop iteration creates an additional If-else term. If the loop is unbounded, then theoretically the formula complexity is infinite. Luckily, in Ethereum smart contracts, loops are typically bounded (e.g., due to gas constrants). Thus, loops may be handled in a symbolic executor by unrolling the loops. This technique is part of a family of model checking approaches known as bounded model checking↗ (BMC). This sort of bounding is an underapproximation. SMTchecker supports BMC, but doesn’t support unrolling loops as of the time of writing, which is a weakness (in my opinion).

Finally, note that we aren’t modeling any view functions. We aren’t really interested in them here, because view functions can’t affect contract state. Thus, calls to a view function can never cause WETH to become insolvent.

Proving solvency

We apply the principle of induction to prove solvency in the general sense. In short, our argument for solvency takes the following form:

• Base case: first, show that there exists some state that is solvent.
• Inductive case: Given an arbitrary solvent starting state (inductive hypothesis), show that state remains solvent after any single transaction made to WETH.

One possible initial reaction to this argument could be: “Well, you showed that it remains solvent after one transaction. But what about exploits involving two or more transactions?”

This counter-argument isn’t valid, because in our inductive case, the starting state is any arbitrary solvent state. Consider a hypothetical “two-transaction” exploit. Clearly, the exploit would not render WETH insolvent after the first transaction, as otherwise the exploit would just be a single-transaction exploit. But since the state post the first transaction is solvent, our proof for the inductive case rules out the possibility that some transaction can suddenly render WETH insolvent. Thus, the hypothetical second transaction in this exploit could not exist. This argument applies to three-transaction, etc. exploits as well.

However, this counterargument does show that it is essential that we don’t make any extraneous assumptions or assertions about the arbitrary starting state in the inductive case.

Base case

The base case is trivial. We start with WETH’s initial state (the one where it’s empty) and deposit some money. Obviously, we can still take the money out. We can prove this for specific user addresses with a simple unit test. To prove that it’s valid for all user addresses, we can use symbolic execution.

Inductive case

We model an arbitrary starting state simply with unconstrained variables. For example, balanceOf is just an unconstrained SMT Array mapping from address to uint256. We also model a specific, arbitrary user and their initial deposit (who we will prove to remain solvent) as an unconstrained address and uint256. Lastly, we also model an arbitrary global EVM state. For our purposes, we only really need to model a global mapping of native eth account balances.

balanceOf = Array('balanceOf', AddressSort, UintSort)
allowance = Array('allowance', AddressSort, ArraySort(AddressSort, UintSort))

myUser = Const('myUser', AddressSort)
initialDeposit = Const('initialDeposit', UintSort)

eth_balances = Array('eth_balances', AddressSort, UintSort)

To prevent the solver from generating “nonsense” counterexamples (i.e., ones which are obviously impossible because they are impossible to attain without breaking the rules of the EVM or violating basic mathematic principles), we enforce the following assumptions about our otherwise-unconstrained state:

• myUser != WETH_Address: the user isn’t the WETH contract itself.
• ForAll([a], ULE(eth_balances[a], 120000000e18)): no Ethereum address has more eth than the total supply of eth.

As with our CHC model, we need to “help” Z3 out by providing some additional theorems about sums over arrays. First, an entry in an array can never exceed the sum of all entries. Second, we already proved with our CHC model that the sum of all entries in $balanceO\mkern-3mu f$ is less than or equal to the total eth balance of WETH. Thus, all entries in $balanceO\mkern-3mu f$ are less than the balance of WETH:

• ForAll([a], ULE(balanceOf[a], eth_balances[WETH_Address]))

Note that as a result of this assertion, our model for this second invariant relies on the properties we proved in the first invariant. This assertion is extremely important for guiding Z3 away from “brute force” proofs that are unfeasible to complete for full sized contracts.

We also assert some rules to set up our hypothetical depositor:

• balanceOf = Store(balanceOf, myUser, Uint(0)): The user starts out with no WETH before their deposit. (this is OK because WLOG we can always get to this “known safe state” in real life by simply withdrawing all our WETH)
• ForAll([a], allowance[myUser][a] == 0): The user hasn’t approved anyone already. (otherwise Z3 will generate a counterexample where some approved user steals the WETH)

Next, we construct our brand-new state, and update it by doing a symbolic deposit with our brand-new depositor:

state = (eth_balances, balanceOf, allowance)
state = deposit(s, state, myUser, initialDeposit)

Now we have a starting state that we can prove theorems with. Note that for the reasons discussed previously, we do not impose any other assumptions on our state—meaning that the variables could be in any (sane) configuration.

Performing a symbolic transaction

Now that we have a starting state, we perform a symbolic transaction on it. This is fairly straightforward. Here is how we model an arbitrary, symbolic deposit call:

def symbolic_deposit(s, state, myUser):
    user = FreshConst(AddressSort, 'user')
    value = FreshConst(UintSort, 'value')
    
    s.add(user != WETH_Address)
    s.add(user != myUser)
    
    state = deposit(s, state, user, value)
    return state

We call our symbolized deposit implementation with an unconstrained msg_sender and msg_value. Note that we do require that the msg_sender isn’t WETH itself (impossible because WETH never calls any of its own functions), and that the user isn’t our hypothetical depositor. Note that we’re implicitly assuming here that the depositor isn’t touching his funds before he withdraws. If we didn’t have this constraint, however, the solver will generate spurious counterexamples, as this constraint is part of the final unsat core↗.

We apply a similar approach to all of the external functions: deposit, withdraw, approve, transfer, and transferFrom.

For each of these functions, we first perform the symbolic transaction. Then we simulate a symbolic withdrawal from our hypothetical depositor in the updated state. Finally, we ask the solver to prove that it is unsatisfiable for the depositor’s withdrawal to have failed, or for the depositor to not end up with the same amount of funds they started with.

Note that in our CHC model, a sat result was desirable, whereas in this BMC model, a unsat result is desirable. Furthermore, in CHC, we started with a concrete initial state, and incrementally expanded our reachable states set through recursive application of the state transition rules. Whereas in this BMC model, our starting state is symbolic, but we only perform a single symbolic transaction. There is some interesting duality here between the two modeling approaches.

Results

Running our Z3Py code, we prove that any potential external transaction on a solvent state will keep that state solvent. In other words, solvency is invariant. We can also query the solver for an unsat core↗, which is a minimized subset of assertions that are all needed to achieve the unsat result.

deposit
Unsat core:
* b!1   line 157  initial_state     ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2   line 161  initial_state     myUser != WETH_Address
* b!4   line 77   deposit           UGE(eth_balances[msg_sender], msg_value)
* b!9   line 190  symbolic_deposit  user != WETH_Address
* b!10  line 191  symbolic_deposit  user != myUser
* b!11  line 77   deposit           UGE(eth_balances[msg_sender], msg_value)
* b!14  line 267  proof_deposit     Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok
withdraw
Unsat core:
* b!0   line 156  initial_state     ForAll([a], ULE(balanceOf[a], eth_balances[WETH_Address]))
* b!1   line 157  initial_state     ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2   line 161  initial_state     myUser != WETH_Address
* b!4   line 77   deposit           UGE(eth_balances[msg_sender], msg_value)
* b!20  line 99   withdraw          UGE(eth_balances[WETH_Address], wad)
* b!18  line 202  symbolic_withdraw  user != myUser
* b!17  line 201  symbolic_withdraw  user != WETH_Address
* b!19  line 94   withdraw          UGE(balanceOf[msg_sender], wad)
* b!23  line 272  proof_withdraw    Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok
approve
Unsat core:
* b!1   line 157  initial_state     ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2   line 161  initial_state     myUser != WETH_Address
* b!4   line 77   deposit           UGE(eth_balances[msg_sender], msg_value)
* b!31  line 277  proof_approve     Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok
transfer
Unsat core:
* b!0   line 156  initial_state     ForAll([a], ULE(balanceOf[a], eth_balances[WETH_Address]))
* b!1   line 157  initial_state     ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2   line 161  initial_state     myUser != WETH_Address
* b!4   line 77   deposit           UGE(eth_balances[msg_sender], msg_value)
* b!37  line 126  transferFrom      UGE(balanceOf[src], wad)
* b!36  line 224  symbolic_transfer  user != myUser
* b!41  line 282  proof_transfer    Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok
transferFrom
Unsat core:
* b!0   line 156  initial_state     ForAll([a], ULE(balanceOf[a], eth_balances[WETH_Address]))
* b!1   line 157  initial_state     ForAll([a], ULE(eth_balances[a], MAX_ETH))
* b!2   line 161  initial_state     myUser != WETH_Address
* b!3   line 162  initial_state     ForAll([a], allowance[myUser][a] == 0)
* b!4   line 77   deposit           UGE(eth_balances[msg_sender], msg_value)
* b!47  line 236  symbolic_transferFrom  user != myUser
* b!48  line 126  transferFrom      UGE(balanceOf[src], wad)
* b!49  line 130  transferFrom      Implies(p, UGE(allowance[src][msg_sender], wad))
* b!52  line 287  proof_transferFrom  Not(is_ok(s, new_state, myUser, initialDeposit, starting_balance))
-> ok

The unsat core is interesting because it tells us exactly which assertions were essential for the security of the smart contract, and thus cannot be removed!

Future Work

There are several limitations in this work, which are potential avenues for future research.

First, because the WETH contract is extremely simple, we symbolized the various functionalities by hand. Large parts of the manual modeling and symbolization could be automated by a formal verification framework. This would also reduce the potential for human error while constructing a model.

Second, we did not consider events or return values in our BMC model. These are important for checking whether WETH is ERC-20 compliant. We consider this outside of the scope of this work, as here we are only interested in safety properties of WETH, not strict ERC-20 compliance.

Third, we did not precisely model reentrancy or interprocedural control flow. In BMC, interprocedural control flow is generally resolved through bounded inlining. However, WETH did not contain any interprocedural calls, thus we did not have to consider that. Additionally, while there is the potential for reentrancy due to the use of native ether, WETH sends ether using .transfer, which imposes a gas limit of 2300, which is too low for reentrancy to be a real concern. Reentrancy may be modeled by considering the additional potential transitions and starting states that reentrancy affords.

Conclusion

WETH is an extremely widespread, popular, and critical smart contract. We proved two important properties about WETH: that (1) its totalSupply is always greater than or equal to the sum of the total number of WETH tokens in existence, and (2) that a new user depositing eth into WETH will always be able to withdraw it later, regardless of what transactions happen to WETH in between. We also identified an interesting, albeit harmless, peculiarity with WETH’s totalSupply implementation, because it does not consider SELFDESTRUCT/coinbase eth transfers.

We proved the two invariants using two different, but complimentary approaches. For the first, we used Constrained Horn Clauses (CHC). For the second, we adopted an approach akin to Bounded Model Checking (BMC).

Formal verification via SMT solving is a widespread approach. For example, it’s part of solc’s built-in SMTchecker and also seems to be heavily used in frameworks like Certora. This approach is extremely enticing, because qualitatively, it often feels as if SMT solvers are able to “magically” prove theorems in time polynomial to the bit size of the various formulas. In general, however, a major challenge when following such an approach is unacceptably slow proof times. Even though a constraint system may be “correct”, it may be unreasonably slow to solve because the specific SMT solver (e.g., Z3) isn’t “finding” the proof. Nonetheless, there are a few heuristic solutions we may use to remedy this during proof development.

While developing proofs, it is often useful to significantly reduce the bit sizes of address and uint256 (160 and 256 bits, respectively) to, say, 4 and 8 bits. This aids in debugging proofs, as even if Z3 gets caught in a “dumb” brute-force solution, it’s still likely to complete in a timely fashion—and the sat model or unsat proof will make the brute-force nature of the solution obvious (the proof or model will be huge). The issues causing a brute-force proof can then be readily debugged and addressed in this scaled-down model.

After working with a “scaled down” toy model which the solver quickly resolves, it can then be gradually “scaled back up”, all the while carefully measuring how proving runtime is scaling with the size of the model. For example, you’d prove a toy model where addresses are 4 bits, and uints are 8 bits—then maybe 16 and 16 bits, then 32 and 32 bits, etc. If you notice that proof time is remaining linear (hopefully) or polynomial (less fortunate) with bit sizes, this is generally promising. Overall, this approach can help identify where the bottlenecks are in proving. Those bottlenecks can then be targetted by manually adding “helpful” lemmas to the solver.

Yet another hack is to minimize the model until the minimal set of constraints leading to pathological solver behavior is isolated. For example, you might have 5 transition rules (or constraints), and the solver isn’t finishing. You can try peeling off constraints that, when removed, don’t seem to help the solver finish any quicker. Repeating this until a minimal “core” is isolated, it’s possible to narrow down where a logical bottleneck in the model is. Then, human intuition can be applied to reason about this bottleneck core, and consider whether there are important lemmas that are missing from the model.

All in all, a fully-automatic solution seems out of the question for the forseeable future. For all but the simplest theorems, SMT solvers are not generally sophisticated enough to prove all desired invariants without human intervention or guidance. For example, to prove the first invariant, we had to manually provide helpful intermediate lemmas to Z3 to guide it towards a proof. While proving the second invariant, we had to manually provide a key lemma proved in the first invariant. Without some degree of human intervention, it would seem very unlikely that a fully-automatic solution would have been able to prove the desired invariants for WETH.

WETH is an extremely simple contract. It is an interesting question whether SMT-based formal verification will scale to larger protocols, especially those involving multiple, mutually-interacting smart contracts. It is desirable to formally verify larger protocols, as there are many “critical” contracts beyond just WETH. To name a few, these include Uniswap, Compound, Aave, and Curve. In the future, we hope to see additional formal verification of smart contracts adopted.

About Us

Zellic specializes in securing emerging technologies. Our security researchers have uncovered vulnerabilities in the most valuable targets, from Fortune 500s to DeFi giants.

Developers, founders, and investors trust our security assessments to ship quickly, confidently, and without critical vulnerabilities. With our background in real-world offensive security research, we find what others miss.

Contact us↗ for an audit that’s better than the rest. Real audits, not rubber stamps.

Endnotes

1. As of block 15934960 (November 9, 2022), WETH has been in 125,581,756 transactions. This count includes all “top-level” transactions which call the WETH contract at any point, including via an internal transaction. Transactions are not double counted. ↩