Uniswap V2 Audit Report

Formal specifications and proofs of method-level correctness for the smart contracts in the uniswap-v2-core repository (namely UniswapV2Pair and UniswapV2Factory) were produced using the act specification language and K framework.

An overview of the formal specifications and their proof status can be found in the audit teams CI system at dapp.ci/k-uniswap, and a discussion on the nature of the proofs produced can be found in the Formal Verification section of this report.

The audit team carried out a general code review and security analysis of the smart contracts of uniswap-v2-core, finding 2 bugs:

• 1 medium severity issue Pair: fix to liquidity deflation introduces race condition
• 1 low severity issue Math: integer overflow in sqrt

along with several recommendations regarding gas optimisation and code clarity, which are presented in detail in the Findings.

Most of these improvements were adopted by the Uniswap development team.

The audit team performed a review of the numerical error incurred during contract execution, with a focus on the desirable invariants proposed by the Uniswap development team (e.g. the rounding error, if any, in a swap, favours the pool).

The team did not find any locations where numeric errors violated these invariants, and additionally produced a novel manual proof of correctness for the Babylonian square root algorithm in the fixed precision setting.

The audit team also committed to carry out a general code review and security analysis of the smart contracts in the uniswap-v2-periphery repository.

Another suite of tests, including property based fuzzing tests using the dapp testing framework were developed during this process and are available here. These tests are targeting a now outdated version of the periphery contracts.

This work was carried out on a best effort basis, and the rate of change and state of active development in the periphery means that the review was performed on a cursory level only.

The team recommends more analysis and review to be performed for the final versions of the peripheral contracts before launch.

One medium severity issue was identified in the Router:

• Router: incompatible with token with fees on transfer

The user facing contract UniswapV2Router01.sol calculates the amount a user needs to transfer to UniswapV2Pair.sol in order to perform a mint, swap or burn.

In cases dealing with a token which subtracts a fee on transferFrom, the amount received by UniswapV2Pair is smaller than the required amount to perform a successful swap, causing the whole call to fail when the fee adjusted invariant is checked at the end of swap.

This is only a problem with the router, and additional routers or token wrappers can be used to mitigate this issue.

Dan Robinson discovered a vector by which an early liquidity provider can make it very costly for other liquidity providers to enter, allowing them to monopolize the liquidity pool:

1. Before there is any liquidity in the pool, the attacker sends a small amount of both tokens of the Pair, receiving a small amount of liquidity pool shares ("LP Tokens").
2. They then send a very large amount of the Pair tokens to the contract, and invokes sync.

This deflates the LP token to be worth a large amount of Pair tokens, which can increase the barrier to entry for other liquidity providers to the point where submitting enough tokens to yield 1 wei of LP tokens can cost millions of dollars.

The Uniswap team suggested a fix to this issue which would force the minimum supply of the LP tokens to be 10,000 units, imposing this constraint in both mint and burn. The reasoning was that this would ensure that the liquidity token would allow for enough granularity, even after someone attempted to increase the barrier to entry.

However, this fix introduced another problem, where a malicious liquidity provider could sacrifice 1 wei of LP tokens to effectively render the last 9,999 LP tokens of the contract irredeemable. In other words, the suggested fix could render liquidity providers unable to exit the contract and redeem their original liquidity and fees.

After discussions with the Uniswap team, another solution was finally settled on:

When providing the initial liquidity to the contract (i.e. when totalSupply is 0 in mint), the liquidity provider must sacrifice 1000 LP tokens (by sending them to address(0)).

This mitigates the issue in two ways:

• The granularity of the LP tokens is always at least 1000
• The cost of performing the LP inflation attack increases significantly, as the attacker is now not the sole holder of LP tokens.

This mitigation comes at the expense of introducing an additional cost for the initial liquidity provider, but this cost is expected to be low enough to be acceptable for most tokens. For tokens with a reasonable value per minimum denomination, 1000 wei does not have more than a modest economic value. Note however, that in the extreme case of a Pair for two tokens that are both worth around $1.00 per wei, the up-front cost for the initial liquidity provider will be around $2,000.

The sqrt function of the Math library contract implements the Babylonian method for calculating the integer square root of y, i.e. the largest integer z such that z^2 <= y.

Before uniswap-v2-core@d1c8612e, the initial value to the iteration was given as x = (y + 1) / 2, which results in an integer overflow when y = uint(-1), setting x to zero, leading to a division by zero in the calculation of x_(n+1).

This does not result in incorrect return value for sqrt, but does cause the function to revert unnecessarily. We suggested to change the initial value to x = y / 2 + 1, making sqrt well defined over its entire domain.

A manual proof of correctness of this algorithm is given here.

The name, decimals and symbol attributes of the UniswapV2ERC20 contract were set dynamically in the constructor. However, they were always set to the same value by the inheriting UniswapV2Pair contract, resulting in unnecessary bytecode complexity and gas consumption.

The audit team recommended that either each Pair should be given a unique name and symbol, or these attributes should be set as hard-coded constant in the UniswapV2ERC20 contract.

Based on the following factors, the Uniswap team decided to make the attributes in question constant:

• String manipulation in Solidity is cumbersome and error-prone
• Uniswap V1 exchanges all have the same name and symbol, and no major issues have been observed in the wild

This change was implemented in uniswap-v2-core@cbe801b5.

The forfeit method of UniswapV2ERC20 allowed anyone to burn their liquidity tokens without receiving tokens from the pool in return. It functioned effectively as a donation to all other members of the pool.

While in some situations such donations to the pool are desirable (e.g. Synthetix used token inflation rewards to incentivise liquidity providers in their Uniswap V1 exchanges), the same outcome can be achieved by transferring tokens to the Pair and calling sync to force the reserves to match the balances.

In the interests of minimizing the number of allowed state transitions in the core UniswapV2Pair contract, the audit team therefore recommended that the forfeit and forfeitFrom methods be removed.

The Uniswap team accepted this recommendation in uniswap-v2-core@cbe801b5.

The createPair method of UniswapV2Factory stored the bytecode for a Pair as a raw bytes value set during construction. When deploying a new Pair, the bytecode would have to be loaded into memory from storage, word-by-word. The audit team recommended that this storage variable be removed, and replaced with the .creationCode attribute of the UniswapV2Pair contract, simplifying the code and clarifying intent.

Moving the bytecode out of storage also resulted in a significant gas saving (millions of gas) when creating Pairs, due to the reduction in the amount of expensive SLOAD operations required.

The Uniswap team accepted this recommendation in uniswap-v2-core@f2d40214.

UniswapV2Pair used the number of blocks elapsed between price updates in order to calculate block-weighted cumulative price. While there are valid arguments that block height is a more "objective" variable than the block timestamp, the audit team suggested that this be changed to use the time elapsed, measured by the change in block timestamp since the last price update.

For consumers that sample the Pair's price accumulators less frequently, e.g. oracles seeking to calculate time-weighted average prices over windows of weeks or months, the choice to use block-weighting or timestamp-weighting could result in material differences. Therefore, using block-weighting might create unexpected results for oracles targeting a time-weighted average (which, at least outside of the blockchain setting, is a more economically meaningful figure)

As a concrete example: the mean Ethereum block time has been known to spike by up to double that of its typical level in the weeks leading up to a "difficulty bomb" hard fork. A block-weighted price accumulator could cause an oracle price with a long averaging window to diverge substantially from the time-weighted average price, as computed by other, off-chain sources. To avoid unnecessarily exposing users to these implementation-related quirks, it may be better to use simple time-weighting.

The allPairs array in the Factory is primarily used to maintain a count of all created Pairs and the audit team noted that it could be replaced by a simple counter. The Uniswap team decided to keep the array implementation in case iteration over the array might be required. They were also advised that any code which iterates over the allPairs array should paginate, or otherwise break up the access into constant-gas chunks, and moreover that iterating over the array from an external contract would be very costly, requiring one call per element read.

Since Solidity uses the hash of the slot as the starting position for storage arrays, their maximum length before integer overflow of the array size depends on the slot number at which they are located: maxUInt256 - keccak(uint256(slot)) + 1

For the sake of completeness, and since it is an unusual property for overflow behaviour to depend on the order in which variables are declared in source code, we note that that Solidity provides no protection against the (negligible probability) overflow of allPairs.

The UniswapV2Pair contract depends on three libraries, UQ112x112, SafeMath and Math, providing additional internal functions and custom syntax for uint256 safemath. Including these internal methods in the UniswapV2Pair directly (or inheriting them from another contract) instead makes creating new pairs about 15000 gas cheaper.

Since this change would make the use of custom syntax for uint256 safemath impossible, the Uniswap team decided to not implement this suggestion.

If burn is called when totalSupply is 0, then the call will fail due to a divide by zero when calculating the amounts to be returned to the caller.

When a divide by zero is encountered, Solidity "throws" by executing the INVALID opcode, consuming all of the gas in the initiating call (unlike REVERT), resulting in an unnecessary monetary loss if burn is accidentally called before any LP shares have been minted. Additionally, this division by zero behaviour in Solidity might not be widely known, since it differs from other languages (like the EVM, in which DIV by 0 returns 0).

Additionally, some analysis tools treat an INVALID opcode as an assertion violation, whereas here it is more akin to an unmet precondition. This can lead to false error reporting or otherwise complicate the analysis of the Uniswap contracts using these tools.

As the divide by zero occurs in such a limited set of circumstances, and has such a limited impact, the audit team presented it for informational purposes only and no change was made by the Uniswap team.

In this variant, an actor who can observe unconfirmed transactions can attempt to insert trades before and after the target trade, manipulating the Pair's price in a way that will result in a profit for the front-runner, and a worse price for the trader.

As an example, consider a Pair for ETH/DAI. Suppose a trader sends a transaction to sell 1 ETH. If a front-runner is able to sandwich the trader's transaction between two trades which sell and buy ETH respectively, then it is clear that the state of the Pair when the trader's transaction is executed will result in a lower price of ETH for the trader, due to the front-runner's sale, and that the extent of the price deterioration will depend on the size of the front-runner's first trade (it can be shown by considering the constant product invariant that the relationship is quadratic). After the target trade has executed, the front-runner's second trade is executed, buying back a sufficient amount of ETH to return the Pair's price to roughly where it started.

By following the flow of balances, we observe that the aggregate economic effect of the sandwiching was equivalent to a trade between the front-runner and the trader (with the pool ending up back where they started, having only collected fees from the 3 transactions), however the front-runner was able to effectively choose the price at which the trade happens by choosing the size of their first trade, and so is able to set the price arbitrarily in their own favour. To see that this can still be profitable in the presence of LP fees, it suffices to observe that while LP fees paid by the front-runner are proportional to the size of the sandwich trade, the price impact of the sandwich trade on the Pair's price is quadratic in the size of the sandwich trade, meaning that the sandwich can be made profitable with a sufficiently large manipulating trade, and the trader's loss is only limited by the value of their trade.

A similar method can be used against a liquidity provider who is entering the pool.

The methods exposed on the user-facing UniswapV2Router01 contract contain arguments that allow callers to impose off-chain slippage limits on their orders (AmountOutMin, AmountOutMax), and when set appropriately these parameters can limit the losses to trader front-running. Note however that it might not be possible to eliminate front-running entirely with this technique, since setting the slippage limit too tightly to the market could result in a poor success rate, with the market moving against the trader.

In this second variant, the attacker watches for large trades, and sandwiches the target trade with calls to mint and burn with a very large position relative to the initial size of the pool. The attacker is therefore able to extract a sizeable proportion of the LP fees for that trade without exposing themselves to the price risk inherent to providing liquidity on Uniswap.

Neither the core nor the periphery contracts contain guards against this attack, and the audit team is not aware of any straightforward solution. A minimum lock lock time for liquidity providers, imposed in the core, could potentially help to reduce the profits siphonable with this attack.

Liquidity providers should monitor the activity on Pairs in which they participate to evaluate their exposure to activity of this kind, since it could result in diminished returns.

Some tokens may mutate an account's balance even when that account was not involved in a token transfer. For example, this may be used to implement (positive or negative) interest paid in-kind. An example of such a token is Ampleforth.

This may fail to have the expected economic effect on a UniswapV2Pair. For example, if its balance in a token were to increase outside of the usual interactions, the surplus tokens would be claimable by any account that calls skim (and would not result in the surplus tokens accruing to the pool, as might be expected). The same will occur if someone "airdrops" tokens on a pool by transferring tokens to it. In order to have the tokens accrue to the pool, sync must be called synchronously with the balance update or transfer.

Tokens that charge a fee on transfer break assumptions in the router, and will result in a revert when traded. Depending on their implementation they may also enable a griefing attack in the core.

Transaction fees can be implemented in two ways:

1. Deduct the fee from the amount credited to the transfer recipient
2. Transfer the full amount and deduct the fee from the sender's balance

The audit team is currently not aware of any popular tokens using the second approach, but at least PAXG is known to use the first.

Although the core is able to handle tokens of either type, both approaches are incompatible with the current implementation of the router in uniswap-v2-periphery. The specifics are discussed in Router: incompatible with token with fees on transfer.

Additionally, if tokens of the second type charge fees for zero balance transfers, a griefing attack will become possible where repeated calls to skim would allow an attacker to deplete all of the tokens in the pool as fees.

The Pair stores its reserves as uint112, but expects the balanceOf method of the underlying token to return a uint256. The internal method (_update) responsible for synchronising balances to reserves therefore reverts if the balances are greater than uint112(-1). This method is called during mint, burn, swap, and sync, meaning that a balance of 112 bits or more would block those methods, until skim is called to siphon off the excess balances. This limits the functionality of the contract for tokens where a balance in excess of \( 2^{112} \) may be realistically achieved.

For a normal 18 digit token, uint112(-1) represents a balance of 19,807,040,628,566,084,398,385,987,584 (\(1.9 \times 10^{19}\) or 19 octillion), well in excess of the total supply of any mainstream token.

This limit could however become problematic should a token with a very large number of decimals be used within a UniswapV2Pair. The audit team is unaware of any tokens in wide use with such high precision.

In order to extract pool tokens using swap, an attacker would have to leave the Pair in a state where the product of the Pair's reserves is less at the end of the call than it was at the start. Additionally, it should be impossible to make a successful call to swap that fails to compensate liquidity providers for the usage of their funds.

Specifically the following formula must be satisfied:

This ensures that:

• The constant product invariant is not violated
• Liquidity providers are paid 0.3% of the value of the inputs to the swap

It should be noted that the above invariant is defined over the Pair's reserves, instead of its balances.

This check is similar, but not exactly equivalent. Semantically reserves can be thought of as "last recorded balances". This has the potential to be problematic as balances are arguably the thing that the UniswapV2Pair really cares about.

All methods that modify reserves or balances (skim, sync, mint, burn, swap) ensure that both are exactly matched at the end of the call. Assuming a non deflationary token, the only way to force a divergence is to transfer tokens into the Pair.

We can therefore infer a system invariant for well behaved tokens: balances are always greater than or equal to reserves at the end of every call to UniswapV2Pair.

Assuming that both of the above invariants hold we can also make some (weaker) statements about the behaviour of the constant product invariant over balances: although it is possible for the product of balances to decrease, these violations are bounded by the product of the reserves, and will in normal operation only manifest themselves through improper usage of the core (token transfer to the pool outside of an atomic sequence of transactions).

The solidity implementation of the invariant check differs from the idealised invariant above in two important ways:

1. Arithmetic Overflow and Numeric Range

   The solidity implementation operates on unsigned integers, and all calculations (except that for the input amounts discussed below) revert on overflow.

   This poses no concern to safety: the invariant check is correct over the domains for which it is defined, and the domain is large enough that liveness is not threatened.

2. Calculation of Inputs

   The calculation of input amounts does not revert on underflow. Negative inputs are instead coerced to zero. This is a design decision made to ensure that the core can handle tokens that deflate the sender's balance on transfer (perhaps as an implementation of some transfer fee). Neither the audit or Uniswap dev teams are aware of any mainstream token implemented in this manner.

   Semantically a negative input amount means that either:

   • balances were less than reserves at the start of the call
   • more than amount{0,1}Out tokens were transferred away from the Pair during the call

   Since a negative input represents a net outflow from the contract, it is not appropriate to charge fees on them, so their coercion to zero (and the associated zero fee adjustment term) does not represent a loss for the liquidity providers.

   The balances at the end of the call will reflect any unexpected shortfall or additional outflow, and the fee adjusted product of the balances at the end of the call must still exceed the product of the reserves at the start of the call. This coercion to zero does not therefore provide an avenue for a malicious caller to exploit the Pair.

For the purposes of this analysis, we assume that the attacker is able to modify all blockchain state during execution of their code, except that which is protected by the mutex in the Pair.

This means that the following state transitions are unavailable during the execution of the callback:

• skim
• sync
• mint
• burn
• swap

Malicious code is therefore unable to:

• modify reserves
• mint or burn LP shares
• transfer pool tokens away from the Pair

It should be noted that not all methods on the Pair are protected by the reentrancy lock. Reentrant calls into the various LP share ERC20 methods (approve, transfer, transferFrom, permit) are possible. These methods do not modify state that is important for the invariant check.

The audit teams believes that these limitations are enough to ensure that an attacker cannot use reentrancy to subvert the fee adjusted invariant check: all inputs to the calculation are either fixed at the start of the call (output amounts), or protected by the mutex (reserves, balances).

There is numerical error when computing the price accumulators, which has no direct economic impact on the pool itself. Consumers of accumulator data, such as oracles, should take care to ensure that the error is within acceptable bounds for their use case. Note that if a token has very low granularity, and the Pair's token balances are low, the effect of rounding down could be too high to viably use the Pair as a price oracle.

There are two square root computations, used to calculate the change in the \( k \) invariant since the last call to _mintFee. In principle, this can result in liquidity providers being charged a slightly higher fee than what they should be charged "in theory", if the second sqrt calculation happens to have a larger error than the first. However, this is not economically significant since the error is small, and most importantly does not accumulate and is bounded in time.

There is also division which rounds against the fee recipient, i.e. in favour of the existing liquidity providers.

sqrt is used to set the initial LP token supply to the geometric mean of the initial supplied token amounts. Numerical error in this situation doesn't appear to have any economically relevant impact, especially in the presence of the minimum supply mitigation.

There is a division when calculating the amount of LP tokens to grant to a new contributor to the pool. The possible error here is in favour of the existing liquidity providers in the pool.

There is division when calculating the amounts of tokens to return to a user leaving the pool. The possible error is against the user, i.e. in favour of the liquidity providers who remain in the pool.

There are no operations that can introduce numerical error in swap. Instead of computing the amount to pay in exchange for the amount received (or vice-versa), the user is allowed to choose both quantities and the contract simply checks that the constant product invariant has increased by the desired amount as a result. This pushes potential rounding errors out to the caller, ensuring that numerical error cannot cause the invariant to be violated.

The specs as written define the functional behaviour of the invocation of a single call to a method of the contract (functional specifications).

They do not, per se, make claims about invariants that should hold across multiple calls (contract level invariants), such as the \( x y = k \) constant product invariant (or its fee-adjusted counterpart).

The team believes that the specifications could in principle be extended to make claims about invariants at the contract level (see here for more details), but time contraints meant that such claims were not pursued as part of this engagement.

UniswapV2Pair calls into untrusted external contracts to get token balances (balanceOf) and to make token transfers (transfer). These calls could result in any behaviour, and in order to simplify the proof work, a token implementation that semantically matches the one in uniswap-v2-core/contracts/UniswapV2ERC20.sol has been assumed.

The proof claims are known to be valid in this context only, and in order to make formal statements about the properties of individual Pairs whose tokens may semantically deviate from this assumption, one would have to generate a new set of proofs for that token.

It should be noted that a malicious token could confiscate or burn the reserves of a Pair that included that specific token. The scope of such an attack is limited to Pairs for which the malicious token is one of the two tokens in the Pair. The loss would fall on the liquidity providers for that Pair, therefore liquidity providers should carefully audit the token implementations for each Pair that they participate in before contributing funds.

There are both theoretical and practical challenges with formally verifying implementations of iterative or recursive numerical algorithms. To verify the correctness of the sqrt implementation, one would have to check numerical error and convergence, in a fixed-precision setting, while also proving convergence and termination. A full bytecode level proof of sqrt would therefore be difficult and time-consuming to produce.

Due to time constraints, its implementation has not been formally verified. Instead, in proofs relying on the result of sqrt, a formal symbolic expression was used, meaning that the specs assert only that storage has been updated with the result of calling sqrt, but do not make any claims about what that result is. Note that this also assumes that the computation always terminates, assuming an adequate amount of gas was provided.

Particular care and attention has been paid to the implementation of sqrt, including fuzz testing, manual review, and a manual proof of correctness of the chosen algorithm in a fixed precision setting. The team discovered one subtle overflow issue. After this issue was resolved, the team is confident that the implementation is suitable for use.

If callers of swap provide a non empty byte array as the data argument, a call into a user provided address will be carried out from the Pair as part of the execution of the swap.

Calls into unknown code pose a significant challenge for the K prover. Without knowledge of the bytecode at the target of the call, the prover is unable to proceed with symbolic execution and can no longer reason about the state of the blockchain. In fact, speaking formally, one must assume that potentially all blockchain state could have been modified in some way by a call into unknown code. Making formal statements about blockchain state after such a call is therefore quite challenging, and to the team's knowledge, full formal verification of an Ethereum smart contract containing a call into unknown code has never been completed.

The team believes that the presence of the reentrancy mutex in UniswapV2Pair in combination with some custom lemmas should allow for the generation of such a proof (see Verification of external calls to unknown code), but time constraints meant that it was not pursued as part of this engagement.

The team has paid careful attention, and devoted much time to considering the potential misuse of this facility, and are unaware of any cases where its use could result in a violation of the fee adjusted constant product invariant, barring pathological token behaviours.

The formal specifications make claims only about the state of the blockchain at the start and end of a call into the Uniswap contracts. They do not make claims about the particulars of any state transitions during a call. This means that the behaviour of the reentrancy mutex is not fully specified. The team has generated proofs of the following:

• The mutex is in the unlocked state at the start and end of all calls
• Calls into the contract will fail if the mutex is in the locked state

The specifications do not however make any claims about the transition from the unlocked to the locked state and back again within the call.

The team has paid close attention to the implementation of the mutex at the source code level, and in the resulting bytecode. Additionally, tests showing the correct functioning of the reentrancy lock have been written and observed to pass.

Proofs of so called ABI exhaustiveness have been generated, meaning that the specs are known to cover all methods on the contract. Proofs of full exhaustiveness (that the specs cover the behaviour of the contract with all possible calldata values) are however not currently generated.

The team is aware of the following instances of unspecified behaviour:

• The implementation of sqrt
• The call into unknown code in swap
• Overflow of the nonces counter in permit
• Overflow of the allPairs array
• Calls to swap when token0 == token1
• Calls to swap when the to address is the address of the Pair itself
• Calls to swap when blockTimestampLast overflows
• Calls to burn when totalSupply == 0
• Calls to burn when the caller is the feeTo address
• Calls to burn when the to address is the address of the Pair, when feeTo =/= 0 or kLast == 0

The sqrt and call into unknown code in swap cases are discussed in their own sections above. In the remaining cases, the decision was taken to deprioritise coverage of unlikely situations to both simplify specification and focus the teams effort on cases that were considered to be the most critical.

A bug in klab or any of its dependencies could invalidate the proof results, or result in faulty specs being incorrectly accepted by the prover. The correctness of the generated proofs relies on the correctness of all of:

• The implementation of the act specification language within klab
• The K EVM semantics
• The K Framework Theorem Prover
• The Z3 SMT Prover

Generating the proofs required in many cases the introduction of various additional assumptions (sometimes referred to as lemmas). These assumptions are typically very narrow technical lemmas, which are infeasible to reason about with SMT solvers, but which can be easily proven mathematically. Although the team has taken care to document and justify these assumptions, an error here could potentially invalidate any proof.

The lemmas and their supporting documentation can be found in k-uniswap-v2/src/lemmas.k.md and k-uniswap-v2/src/prelude.smt2.md.

Three proof objects are generated for each method:

• pass_rough
• fail_rough
• pass

The *_rough proofs assume that the method is executed using a very large amount of gas (currently 3000000). Once the pass_rough spec has been successfully proven, the trace of the symbolic execution in the proof is used to produce a symbolic expression (G) for the exact amount of gas used by the method (as a function of the state, calldata, etc.). This gas expression is then used to produce the pass proof, which proves the spec under all of the same conditions as the pass_rough spec, but additionally strengthens its claim to say that the amount of gas provided is >= G.

Due to performance constraints in the K prover, a proof that the method will fail if called with a gas value < G is currently not generated. However, the team believes that this claim should in principle be provable.

The audit team believes that the act specs generated as part of this engagement could be extended to prove that core accounting invariants are maintained for every possible combination of calls into a V2 Pair.

The team believes that two potential approaches are viable:

1. Compilation of the act specs into some high level proof language (e.g. Coq, Agda)
2. An inductive proof implemented using post-conditions in the generated K specs

The team believes that the addition of lemmas resetting all EVM state that could potentially have been affected by the call (essentially all state not guarded by the reentrancy mutex) to an abstract value after the conclusion of the call should allow for a successful proof of correctness of the relevant code paths in swap.

The team believes that it should be possible to prove a loop invariant by coïnduction showing the EVM implementation of sqrt agrees with the model used in the manual proof of convergence.