As the DeFi sphere has become more mature and fortified, some classes of bugs are getting much rarer. Reentrancies, access-control bypasses, and first depositor attacks, to name a few examples, are well understood by both web3 security researchers and developers. Therefore, we see that such “classical” attack vectors have almost become a thing of the past. But there seems to be one class of bugs that is still going strong even in 2025 - rounding errors. Losses from rounding errors in the last two years exceed $100M USD.

In this blog, we will present rounding errors and show how even small inaccuracies, off by 1 wei, can grow into critical exploits. We will explain why these errors, while hard for humans, are easy to find via automated formal verification. Finally, we will demonstrate how we used these techniques to find bugs in a live protocol.

But hey! How can a result that is off by one wei (e.g. 1E-18 ether) lead to a critical bug? Obviously, we do not consider an attacker scoring extra wei from the protocol a grand theft. However, in some (but not all!) cases, rounding errors can have a huge effect through one of several mechanisms:

• One wei is crafted to be worth a lot, such that each rounding error is crucial, for example, when a protocol accidentally rounds down to zero instead of one. This can happen in cases where we incorrectly round down shares that represent ownership of funds or skew a liquidity pool of multiple tokens (e.g. ZkLend (2025), Abracadabra (2024), Wise Lending (2024), Hundred Finance (2023), Raft (2023))
• One wei makes a drastic change in the execution of the contract, such as a new code branch, which is inadvertently taken (e.g. KyberSwap (2023)).
• One wei is worth enough to run the attack repeatedly. This happens mostly in blockchains with very low gas costs to make this profitable (SPL Swap (2022), Yieldly (2022))

But how can something as small as a rounding discrepancy, often just one wei, cause millions in damage? To understand that, we need to look under the hood and see why these bugs are both inevitable and so difficult to catch.

Because EVM only supports integer numbers, every time a developer needs to implement some division operation (e.g. for ratio calculation or unit conversion), they have to decide whether to round the resulting real number down, up, or to the nearest integer. Each decision leaves an opening for a rounding error. Though there are some established rules of thumb (“always round in favor of the protocol”), many times, there is only the hope that the rounding issues couldn’t be scaled up to a critical level. In a sense, rounding errors are inevitable.

So, why haven’t we managed as a community to eradicate rounding errors like we were able to do for other classes of bugs?

Rounding errors are hard for humans, easy for computers

I believe that rounding errors are notoriously hard to uncover by both the protocol’s programmer and the security researchers auditing the protocol, because humans are bad at reasoning on the kind of logic required to find rounding issues. Usually, we can grasp quite well the entire logical state machine of a given protocol and mentally try to poke holes in it:

• Can an attacker repeat a transaction to allow double-spending?
• Does the protocol allow the owner to steal funds?
• Can a change of protocol parameter cause an irreversible denial-of-service?

Those kinds of questions, once posed, are easily verifiable by a human. On the other hand, rounding errors require more mathematical reasoning (and over integers nonetheless!), which, unfortunately, we do not excel in.(  As an example, see our blogpost Problems in Solidity Fixed Point Libraries)

In the simplest cases, we would see something like this:

function convertToShares(uint256 assets) public view virtual returns (uint256) {

        uint256 supply = _totalSupply;

if (supply == 0) {

    return assets

        }

return (assets * supply) / totalAssets();

    }

Here, we see a conversion between assets and shares in an ERC-4626 vault. Evidently, the number of shares returned by this function is rounded down due to the nature of the division operator in solidity. This is indeed on par with the ERC-4626 guidelines, and can be verified with very little effort.

But many rounding scenarios are far less crystal clear. As a more elaborate example, consider the following Solidity function, which implements a price calculation for a swap. Ignoring the context, can you tell if the rounding directions are consistent?

function estimateIncrementalLiquidity(

   uint256 absDelta,

   uint256 liquidity,

   uint160 currentSqrtP,

   uint256 feeInFeeUnits,

   bool isExactInput,

   bool isToken0

 ) internal pure returns (uint256 deltaL) {

   if (isExactInput) {

     if (isToken0) {

       deltaL = FullMath.mulDivCeiling(currentSqrtP,absDelta * feeInFeeUnits,TWO_FEE_UNITS);

       uint256 tmp = FullMath.mulDivFloor(absDelta, currentSqrtP, TWO_POW_96);

       FullMath.mulDivCeiling(liquidity + deltaL, currentSqrtP, liquidity + tmp);

     } else {

       deltaL = FullMath.mulDivCeiling(C.TWO_POW_96,absDelta  feeInFeeUnits,TWO_FEE_UNITS  currentSqrtP);

       uint256 tmp = FullMath.mulDivFloor(absDelta, TWO_POW_96, currentSqrtP);

       return FullMath.mulDivFloor(liquidity + tmp, currentSqrtP, liquidity - deltaL);

     }

   }

   else

     {

       uint256 a = feeInFeeUnits;

       uint256 b = (FEE_UNITS - feeInFeeUnits) * liquidity;

       uint256 c = feeInFeeUnits  liquidity  absDelta;

       if (isToken0) {

           b -= FullMath.mulDivFloor(C.FEE_UNITS * absDelta, currentSqrtP, TWO_POW_96);

           c = FullMath.mulDivFloor(c, currentSqrtP, TWO_POW_96);

           deltaL = QuadMath.getSmallerRootOfQuadEqn(a, b, c); //(b - sqrt(b  b - a  c)) / a;

           uint256 tmp = FullMath.mulDivFloor(absDelta, currentSqrtP, TWO_POW_96);

           return FullMath.mulDivFloor(liquidity + deltaL, currentSqrtP, liquidity - tmp);

     } else {

           b -= FullMath.mulDivFloor(C.FEE_UNITS * absDelta, TWO_POW_96, currentSqrtP);

           c = FullMath.mulDivFloor(c, TWO_POW_96, currentSqrtP);

           deltaL = QuadMath.getSmallerRootOfQuadEqn(a, b, c); //(b - sqrt(b  b - a  c)) / a;

           uint256 tmp = FullMath.mulDivFloor(absDelta, TWO_POW_96, currentSqrtP);

           return FullMath.mulDivCeiling(liquidity - tmp, currentSqrtP, liquidity + deltaL);

     }

     }

 }

Naturally, the answer is no (I’m not a sadist!). In the case where isExactInput is true and isToken0 is false, there is an inconsistency - deltaL is rounded up, and appears with a minus sign in the denominator of the fraction(This code is based on the Kyberswap’s code involved in the aforementioned incident.). Factoring all in, this means that the fraction is getting larger, which is inconsistent with the rounding down of the fraction. These types of convoluted mathematical conundrums are often the kind of reasoning needed to find rounding errors.

Developers and auditors have a limited time to assess the code before deployment. However, attackers have unlimited time to uncover rounding error bugs. In some cases, white hats have spent over a year on a single protocol to find a critical rounding error. Manual review alone cannot reliably defend against rounding errors.

Unlike humans, computers are excellent at crunching numbers. More specifically, computers are excellent at formal verification (FV) - the ability to prove a mathematical property of a piece of code, and in our case, a smart contract or an entire protocol. In order to employ FV, we need to specify to the formal prover what kind of property we want to verify. The prover could either give us a mathematical proof that the property holds for all the viable states in the protocol state-machine or give us a counter-example (e.g., a concrete state of the protocol and a concrete external function call to one of its contracts that violates the property).

While from a worm’s eye view, rounding issues can seem vague, from a bird’s eye view, they become clear - we can specify general properties or invariants of the code that we know should always hold. For example,

• The price of a share in an ERC-4626 vault should never decrease.
• A pool’s invariant should never decrease unless liquidity is extracted.
• In every interaction of a user with the protocol, a third-party user can’t lose their funds unless they are liquidated.

Had we been able to check these kinds of statements for some of the protocols listed in the beginning, the rounding errors, hidden deep inside the protocol’s business logic, would have naturally popped up as counter-examples that violate the properties.

Rounding errors in the wild - Juice Finance

Juice Finance (or "Juice" for short) protocol is a standard leveraged lending protocol in the Blast blockchain, which at the time of writing, has a few tens of M\$ in TVL. In a standard course of action, a user locks some amount of collateral token and can then borrow another token (up to some multiplier from the amount of locked collateral) to be invested in some yield strategies pre-defined by Juice. 

We wouldn't want to delve deep into the structure of the Juice protocol, but some shallow understanding of its mechanisms is required. Juice is made out of four components:

1. The Lending Pool - Provides liquidation for the borrowed token
2. The Account Manager - Creates and manages (leveraged) accounts
3. Account(s) - Smart contracts created by the account manager per user. Hold the borrowed tokens.
4. Strategies - A set of contracts that allows an account to invest in yielding strategies using the borrowed tokens.

The standard flow of the protocol is as follows: User A deposits some borrowed token (currently USDB or WETH) to the Lending Pool, and gets interest-bearing liquidity tokens. User B asks the Account Manager to open a new account, which he will own. He provides collateral (using AccountManager.deposit()), which grants him non-transferable ERC-4626 collateral share tokens. He can then borrow some tokens to his leveraged account, which is accounted for using fictitious debt tokens minted for the account. The Account Manager makes sure that the account is healthy, meaning that the amount of collateral locked by the Account's owner plus the current amount of borrowed tokens in the account itself, divided by the amount of debt tokens the account has, is more than some threshold. From here on, the user is allowed to invest his borrowed token in a concrete set of yield strategies that are implemented by the protocol (using accountManager.strategyDeposit()). Later on, pending a successful yield, the user is allowed to claim profits (using account.claim()).

The liquidation flow is more convoluted than usual, as it is composed of several separate liquidation calls to the Account Manager. Here, we will just denote one of the calls, AccountManager.liquidateCollateral(), which seizes collateral from an unhealthy account, sells it for borrowed tokens, and uses these to repay the debt.

Formal verification and violations

At Certora, we have a few “golden rules” that we always try to prove (or disprove) for every lending protocol, including :

1. A lending position can’t be driven into an unhealthy (liquefiable) state other than by a price change or an interest accumulation (see more about this in our blog post “The Holy Grail”).
2.  Liquidations must succeed for an unhealthy position (up to some obvious requirements, such that the liquidator has enough funding to carry the liquidations).

When running the first property, we’ve discovered two cases where a user can drive either themselves or other users into an unhealthy state. In the first case, the prover discovered that the AccountManager.deposit() rounds incorrectly the amount of shares minted to the account, such that the share’s price decreases instead of increases. This, in turn, can make a third-party user's account unhealthy. This occurs because the ERC4626 previewDeposit() function performs two rounding-down operations (one from assets to shares and one back from shares to assets), effectively rounding up the amount of minted shares.

In the second case, a user can liquidate themselves because the AccountManager.repay() method rounds down the amount of shares to be burned (which naively sounds correct), which can drive the user position over the liquidation threshold line. This is possible because unlike in the case where a user borrows a loan or withdraws collateral, when a user repays a loan, the system doesn’t check the health status of a user’s account (because of an incorrect assumption that repayment of a loan can never decrease the health status).

As for the second property, the Certora prover discovered an edge case where a specially crafted position is non-liquefiable. This occurs during the call to accountManager.liquidateCollateral(), when the system tries to transfer the liquidated account’s assets to two parties - to the liquidator (msg.sender) and the beneficiary of the liquidation bonus (liquidationFeeTo), by two subsequent calls to _withdrawAssets(), which rounds up the amount of shares to burn for the account. Like the previous case, this sounds reasonable, as we round against the liquidated account. However, because the rounding-up is happening twice, the system would try to burn more shares than the account actually possesses (this happens when the two rounding-up fractions add up to more than one). Therefore, an attempt to liquidate the collateral of such an account would cause the transaction to revert.

It is important to note that in this case, FV doesn’t deal with the exploitation of the contract but simply points out possible weak points (where certain properties cease to hold) that could be exploited.

Don’t Let Rounding Errors Slip Through

Rounding errors can introduce serious vulnerabilities in DeFi protocols—ones that are often missed during manual audits due to their mathematical subtlety.

Formal verification provides a rigorous, reliable way to detect and prevent these issues. By defining your protocol’s invariants explicitly and verifying them systematically, you can catch critical bugs early and secure your code before it goes live.

If you’re building a smart contract and want to eliminate rounding-related vulnerabilities before they hit production, let’s talk. We’re here to help.