Introduction

Automated Market Makers (AMMs) like Uniswap are foundational to decentralized finance (DeFi), enabling trustless trading and liquidity provision. One critical expectation from liquidity providers (LPs) is that they can always withdraw their funds, even in a worst-case scenario like a bank run. But how can we formally prove that an AMM always has enough liquidity to meet its obligations?

This post delves into Uniswap v4’s liquidity mechanism and outlines a formal methodology to prove its solvency. By leveraging mathematical invariants and SMT solvers, we demonstrate how liquidity is always maintained and how these methods can be extended to other DeFi protocols.

What is an AMM?

An AMM (automated market maker) is a decentralized exchange that facilitates trades between liquidity providers and traders. Liquidity providers provide the tokens that can be traded and a rough price range in which they want to allow trades.

A smart contract automatically adjusts the trading price based on supply. If the supply of one token decreases (because traders buy this token from the contract), the price increases. The price decreases if the supply increases (because traders sell it). 

The liquidity providers earn a fee from every trade, but they do not influence whether their tokens are sold or bought. The traders pay the fee to liquidity providers and profit from the instant fulfillment of their sell or buy order.

Key Features of an AMM:

• Liquidity providers (LPs) earn trading fees but have no direct control over transactions.
• Traders swap tokens instantly at algorithmically determined prices.
• Smart contracts manage liquidity autonomously, ensuring trustless execution.

What is Solvency in an AMM?

Solvency refers to the availability of assets within an AMM contract, particularly the liquidity provided by LPs, to facilitate trades. For an AMM to be considered solvent, it must always have enough funds to satisfy all LP withdrawals.

Ensuring Liquidity:

• LPs receive certificates representing their stake in the pool.
• These certificates allow LPs to withdraw their share of the liquidity at any time.
• The AMM must always maintain a balance that matches these obligations.

How Do We Formally Prove Solvency?

A property that should always hold is also called an invariant. In our case, the invariant is that the contract has enough funds to pay out the liquidity providers. To prove that an invariant holds, one can look at any function separately and argue whether the function can violate the invariant, i.e., if there is a transition from a state where the invariant holds to a state where the invariant does not hold. The key invariant we aim to prove is:

The contract always has enough funds to pay out all LPs.

To verify this, we analyze each function in the smart contract to ensure it does not lead to a state where this invariant is violated. The methodology involves:

1. Translating code into mathematical formulas.
2. An SMT solver is used to verify that liquidity is maintained across all function calls.
3. Generating counterexamples if any function breaks the invariant.

For this, we translate the code of a function into a mathematical formula. We then ask an SMT solver whether enough_funds@before && function → enough_funds@after holds for all possible starting states and all function parameters. We do this for any public function in the contract. If the formulas are always true, we have mathematically proven that the contract will always have enough funds. If the formula is false for some inputs, the SMT solver can provide a counterexample that explains under what conditions the invariant can be violated.

Applying this to Uniswap v4

For Uniswap v4, the swap function is critical as it computes token amounts based on an internal liquidity variable (pool.liquidity). If this value is incorrect, the calculated token amounts may be wrong. Our proof ensures that:

• Liquidity is always correctly computed as the sum of all active positions.
• No function transition breaks the liquidity invariant.

This diagram illustrates the state space of the Uniswap PoolManager. The blue circle represents the set of states in which the contract maintains sufficient funds (i.e., remains solvent). Arrows depict potential state transitions resulting from calls to the contract's public functions. The cloud shape encloses all states that are reachable from the initial state via these transitions. Ideally, the cloud would lie entirely within the blue region, ensuring that every state reached is solvent. 

However, as illustrated, some transitions—such as invoking the swap function when liquidity is miscalculated—lead outside the blue region. By introducing additional constraints, we can define a smaller yellow region that still encompasses all reachable states and for which every transition originating from a state within this region remains inside it. This yellow region is an inductive invariant, rigorously proving that the contract always has sufficient funds in every reachable state.

We apply the proof technique to a concrete example: the Uniswap v4 pool manager. For this contract, the invariant “enough funds” can be violated by the swap operation. The function swap computes the token amounts based on an internal variable pool.liquidity. If this variable has the wrong value, the token amount computed by swap is wrong. However, in all reachable states, this variable is computed correctly as the sum of the liquidity in all currently active positions.

In general, to prove that an invariant holds, one may need to prove more invariants simultaneously, such as that the sum of the liquidity in all active positions equals pool.liquidity.  In Uniswap, the LP can choose the price range where a position is active by providing a minimal and maximal trading price in ticks.  

To prove this new invariant, even when positions are activated or deactivated by price changes, we also need to show a third invariant, namely that for any tick, ticks[tick].netLiquidity is equal to the difference between the sum of liquidity in positions starting at tick and the sum of liquidity in positions ending at tick.

Once we have enough invariants, their combination is an inductive invariant: no transaction leads from a state satisfying the inductive invariant to a state not satisfying it. In addition, we need to show that the invariants hold after calling the constructor. Then, we have formal proof that these invariants hold for all reachable states.

How Much Funds Are "Enough"?

To accurately determine the funds required, we categorize them within Uniswap v4’s contract:

• Liquidity in pools (token reserves for trading pairs).
• LP trading fees (accumulated but not yet withdrawn).
• Protocol fees (collected by the Uniswap DAO).
• ERC-6909 token reserves (backing synthetic tokens).
• Temporary currency deltas (pending transactions or flash loans).
• Temporary debt in the middle of an operation

The last two entries are temporary and can even be negative, implying that the contract provides a flash loan to a user during a transaction. The temporary debt exists only while the post-swap or the post-modify-liquidity hook is called. When the post-swap hook is called, the swap has occurred, but it has not yet been accounted for as a change to the user's currency delta, as the post-swap hook may modify the token amount by giving the user a discount or an additional fee. After the post-swap hook returns, the currency delta is updated, and the temporary debt is removed. The post-modify-liquidity hook works exactly the same way.

The currency delta data structure is transient and exists only when the contract is unlocked by calling the unlock function. This delta is negative if the user has a pending flash loan or positive if the user has received funds (by removing liquidity or by swapping) that they haven’t withdrawn yet. The lock mechanism ensures that all delta entries are zero at the end of the transaction. This ensures that the user pays back all flash loans and withdraws all the funds or mints ERC-6909 tokens for not withdrawn funds.

The ERC-6909 tokens are 1:1 backed by real ERC-20 tokens in the contract. The token's ID is its ERC-20 address, and the tokens are minted by the Uniswap core contract itself. They can be used to avoid transfer fees on ERC-20 tokens by keeping all ERC-20 in the Uniswap core until the user sells them or uses them to add liquidity.

The final invariant equation ensures:

We can introduce a ghost variable and use hooks or summaries for each of these pots. For example, the currency_delta is updated by the library function CurrencyDelta.setDelta.  We summarize this function and keep the sum of all currency_delta of all accounts and one token in a ghost variable.

For liquidity, the ghost variable provided_liquidity[token] is the sum of all token liquidity for each pool. We introduce ghost variables for each pool to store the expected token amounts. In the next section, we will explain how to compute this amount.

Required Tokens for Pool Liquidity

The liquidity for a token pair in a constant product pool is the geometric mean of the provided tokens, i.e., if a and b are the number of provided tokens for each of the two tokens in a token pair in the AMM, then the liquidity is liq = √(a · b)  In addition, the liquidity provided in both tokens must have the same valuation with respect to the current price, i.e. price = b/a.   It’s easy to derive from these equations the equations for computing the token amount from the liquidity:

Example:

Assume the current price is 2500 USD/ETH, then the square root of the price is 50.

We assume 18 digits for both tokens, so 1 USD and 1 ETH are represented as 10^18.

Providing 1 ETH & 2500 USD gives you a liquidity of √(2500 · 10^36 ) = 50 · 10^18

The number of ETH is obtained by dividing the liquidity by the square root of the current price, giving 1 ETH, and the number of USD is obtained by multiplying the liquidity with the square root of the current price (50), resulting in 2500 USD. If the price moves to 1600 USD/ETH (square root price is 40), the user now owns 1.25 ETH and 2000 USD.  

The ETH gained, and USD lost is due to traders who sold ETH for USD, which caused the ETH price to drop and also changed the number of tokens the Uniswap contract now holds for this pool. This ensures that:

• The ratio of token reserves aligns with the current price.
• The liquidity pool can facilitate trades while maintaining solvency.

Concentrated Liquidity Model

Instead of providing liquidity for the full price range, the LP can provide a minimum and maximum price range. They then don’t supply all the tokens for liquidity, but only the part that is traded between the price range. As long as the price is outside the price range, their position is dormant, and they only own one side of the tokens.

Example (continued):
Let's assume that a Liquidity Provider (LP) selects a price range between 1600 and 6400 USD/ETH and provides 50 · 10^18 liquidity. At the lower bound of 1600 USD/ETH and without concentrated liquidity, the LP would possess 1.25 ETH and 2000 USD. Conversely, at the upper bound of 6400 USD/ETH, they would hold 0.625 ETH and 4000 USD.

Rather than contributing the full liquidity amount of 1 ETH and 2500 USD, the LP only needs to input 500 USD and 0.375 ETH into the contract. This is strategically done so that their balance diminishes to 0 USD at the minimum price and to 0 ETH at the maximum price.

Should the price surpass 6400 USD/ETH, the LP retains 2000 USD from their position and no ETH. This effectively means the user sold their 0.375 ETH for 1500 USD at an average price of 4000 USD/ETH. The LP doesn't require the additional 2000 USD and 0.625 ETH and can maintain the same liquidity level using fewer resources. This strategy is called concentrated liquidity, as a user attains the same liquidity with a reduced capital commitment but only within a specified trading range.

With concentrated liquidity, the equations for the amount of tokens for a single position can be computed as:

To avoid computations of square root, the Uniswap contract stores the value √price in the field cursqrtprice, and the functions that compute the price for a tick already return the square root of that price.  More precisely, the cursqrtprice is stored as a fixed point number, i.e., as 2^96√price, and is always an integer (the swap function ensures this).

One tricky aspect is that we must avoid rounding errors when computing the number of tokens. If there are rounding errors, any price change can add more rounding errors, which may increase the required token amount by several tokens if there are many small positions. Thus, rounding errors can break the invariant when swapping. 

To avoid rounding errors, the first trick is to represent all prices as their square root, as mentioned above, so there are no rounding errors.  Furthermore, we do not store a and b, but we multiply the quantities by superprecision, which is a very large number that is divisible by any number below 2^256. We can do this because the ghost variables in CVL are unbounded integers and can be arbitrarily large. By multiplying the quantities with this large number, we ensure that a*superprecision is always an integer, eliminating the possibility of rounding errors. For the solver, we can keep superprecision symbolic so that we never have to write down this number.

Handling Rounding Errors

Computational rounding errors can lead to discrepancies in liquidity calculations. To counteract this:

• Liquidity values are stored as high-precision integers.
• No rounding errors in the specification through ghost variables and symbolic computation with unbounded integers.

ERC-20 Considerations

Assumptions and Requirements for ERC-20 Tokens in Uniswap

Uniswap can be used with any ERC-20 token, but solvency can only be assured for tokens that follow specific rules:

• balanceOf() has no side effects and only queries the account balance.
• The account balance can only be decreased by the owner and approved spenders.
• The balance only decreases when calling the transfer/transferFrom function of the token.
• A spender can only be approved by the owner and only by calling approve.
• The function transfer(receiver, amount) decreases the sender’s balance by the exact specified amount.
• The function transfer won't revert if the sender has enough balance.

Important Considerations

• Some commonly used tokens do not fully meet these assumptions under certain circumstances. For example, rebasing tokens like stETH are not supported by Uniswap v4—using them can lead to lost funds—while Synthetix is analogous to Celo and is technically supported in the final version of Uniswap v4. However, our proof does not cover it. 
• Finally, USDC has a blacklist function that could, in theory, block the Uniswap contract from paying out liquidity providers; however, this scenario is widely regarded as highly unlikely.
• The proof of AMM liquidity doesn't prevent all losses. For example, if the token charges a fee, the user may receive less than the transferred tokens.
• The requirement that the token be non-double-entry breaks the version of Uniswap v4 provided to auditors in August ‘24 on chains like Celo, where the native token has an ERC-20 mirror token. The final version of Uniswap v4 fixed this issue.

Conclusion

Formally proving solvency in an AMM like Uniswap v4 enhances security and user trust. By leveraging mathematical proofs and automated solvers, we:

• Ensure AMMs maintain solvency under all conditions.
• Identify and mitigate potential rounding errors and token inconsistencies. No new rounding issues were found.
• Strengthen DeFi security through rigorous verification methods.

The DeFi ecosystem can minimize smart contract vulnerabilities by adopting formal verification techniques, paving the way for a more robust and resilient financial infrastructure.

Get your Uniswap v4 audit now! Ensure the security of your Uniswap v4 hook implementation with a formal verification audit. Contact Certora for a comprehensive smart contract audit of your Uniswap v4 hooks and get your contracts formally verified today.