How the AuditHub Approach Would Have Flagged Future Protocol’s $4.6M Bug: Pre-Mortem

Pre-Mortem is a weekly series by Kostas Ferles, CTO of AuditHub. This article looks at a token that charged its sell tax to a liquidity pool instead of the seller, and at the check that catches it. New breakdown every week. Find Kostas at @KFerles.

This article shows how we can catch a bug like this with an invariant. And the best part? The invariant does not even have to mention the vulnerable path.

Jon Stephens covered this one from the reviewer’s side in this week’s Auditor’s Take [LINK AT PUBLISH]. Here is what happened.

FPC applied a fee whenever a transfer landed on its PancakeSwap FPC/USDT pair, which is what a sale looks like from inside the token. That fee came out of the pool’s holdings rather than the seller’s, sync ran next, and the remaining tokens arrived after that. The middle step is the bug, and the next section walks it.

On July 2, 2025 an attacker flash-loaned 23,020,000 USDT and swapped all of it for FPC, leaving 160,836 FPC in the pool. Sending 247,441 FPC back triggered that sequence, and the pool’s books ended up reading 0.000065 FPC against an unchanged USDT balance. The swap that followed paid out 27,693,883 USDT, roughly $4.6 million more than repaying the loan cost.

The two contracts looked correct individually, but their composition was vulnerable. The pool ran its ordinary accounting, the token ran its own fee logic, and the loss came from the order in which the token drove them. So the question for a development team is what would have caught this before it shipped.

TL;DR

• FPC burned the fee from the pool’s balance, then called sync before transferring the rest in.
• Reserves fell to 0.000065 FPC; the pool then quoted 27,693,883 USDT and paid it.
• OrCa checks one property, that the reserve product never decreases, whatever the cause.
• The counterexample comes back as a runnable Foundry test, not a warning to triage.

Why a Pool Has No Defense Here

A Uniswap V2 pool tracks two things that are easy to run together: the token balances it actually holds, and reserves, a stored snapshot of those balances. Pricing reads reserves, never the live balances, and the two are not kept in lockstep. Send tokens to a pool and its balance rises immediately while reserves sit where they were.

Two functions close that difference, and anyone may call either. sync overwrites reserves with the current balances. skim leaves reserves alone and sends the surplus to the caller. Both were written for a pool holding more than its reserves claim, so neither checks the product.

FPC’s transfer to the pool ran three steps, and the order is the whole bug. Follow the balance and the reserves separately:

1. Burn the fee from the pool’s holdings. The balance drops. Reserves have not moved, so they still describe the pool as it stood a moment earlier.
2. Call sync. Reserves are overwritten from the balance as it stands right now, which is its lowest point in the operation. In the July transaction this is the step that left reserves reading 0.000065 FPC.
3. Transfer the remaining tokens to the pool. The balance rises again. Reserves do not, because nothing calls sync a second time.

The pool comes out of that transfer quoting against a reserve figure captured mid-operation.

The same failure has shown up in other tokens, produced by different code each time. KRC/BUSD on BSC, May 2025: repeated transfers and a skim call, per OpenZeppelin. New Gold Protocol, September 2025, around $2 million: the same ordering, a 35% sell fee taken from the pool and synced before the seller’s tokens arrived, per QuillAudits. BFB, July 2026, 396 BNB: zero-value transferFrom calls driving a 5% burn of the pool’s holdings about 151 times over, per AMBCrypto.

Reviewing the token and the pool separately gets you there eventually. Stay here for the version that does not wait for someone to look.

The Property, Written Down

The pool’s own assumption is short enough to state in a line: no transaction should end with the product of the reserves lower than it started. That is what swap enforces internally, and what sync never checks. Written for OrCa, our specification-guided fuzzer, it looks like this:

Read it as a sentence. finished(*, ...) is the event that any transaction completes, with * meaning no particular entry point is named. The old(...) terms are the reserves as the transaction began, so the condition compares the product after against the product before. The ! says that event must not happen, and the [] says it must not happen at any point in any sequence the fuzzer explores. Together: no transaction ever finishes having reduced the product of the pool’s reserves.

Nothing in it mentions a burn, a recipient check, or sync, and that is the useful part. The spec describes the outcome a pool cannot survive rather than the code that produces it, so it holds against any token that arrives there, including ones whose logic looks nothing like FPC’s. Our benchmark set already contains another token that gets there by different code.

What a Live-State Run Settles

OrCa fuzzes the deployed contracts at a chosen block, using the storage those contracts actually hold rather than an environment assembled by hand. Pointed at the FPC pair with the spec above, it returns a violating sequence:

Two calls, in order. The first funds user0 with 50 tokens. The second is the violation: a plain transfer of 4 tokens from user0 straight to the pool.

Where is the flash loan, and why does it take two calls? There is no flash loan, and no swap. The July drain needed one to be worth the attacker’s time, but the property comes apart on a four-token transfer from an ordinary address. The funding call is only there because OrCa had to reach that state; one call from an address already holding the token does the same thing.

OrCa emits that sequence as a runnable Foundry test, so the first thing a developer does with the finding is run it and watch the product fall.

The run does not show the pool being emptied. It shows that a plain transfer can lower the constant product against the state that actually shipped, and the drain follows from there: the attacker’s next swap priced against reserves that had already moved.

Coverage also starts before anyone writes a spec by hand. OrCa ships a push-button configuration that runs its standard ERC20 properties against a token automatically, and burn-on-transfer behavior is one of the things it reports. FPC comes back as unusual on that first run.

What a Developer Should Take From This

The FPC-shaped lesson is narrow, so here is the wider one. Most protocols are held together by properties nobody has written down. A lending market stays solvent. A bridge releases funds only against a real deposit. A pool’s product never falls. Teams carry these in their heads, enforce them implicitly in a few functions, and learn at exploit time which paths never enforced them.

Writing the property down changes what happens next, because it stops depending on someone thinking of the attack first. The spec describes the outcome rather than the route, and the fuzzer goes looking for routes nobody modeled. FPC is a good argument for that: the burn was conditioned on the recipient’s address and buried in a recursive internal call, which is not a path a reviewer would think to guess, and the spec did not have to guess. Beanstalk was the same shape with entirely different code.

So the practice is to name the properties your protocol cannot survive violating, encode them, and put a tool on them. The list is usually shorter than teams expect.

From a Launch Gate to a Schedule

An audit certifies two contracts as they looked on one day, and this class does not respect that boundary. Whoever creates a pool inherits the transfer logic of the tokens in it, and a new pool against a taxed token can be created by a stranger long after every review closed. Nothing in a diff shows that up, because nothing in the repository changed.

The property is stable while the pools around it keep appearing. That is what continuous security means once a token is live: the same spec runs on a schedule against whatever pairs exist now, so the next pool gets checked the day it is created.

Want to know whether your protocol holds its own invariants?

One branch in a transfer function turned a sell tax into a $4.6M withdrawal nobody authorized. To write your properties down and put a tool on them, try AuditHub for free or book a demo.

What to remember about constant product manipulation

Constant product manipulation detection is the practice of testing an AMM’s reserve invariant against live state, instead of trusting that every path which moves a pool’s balances also checks the product. It catches the class Future Protocol fell to: a fee burned from the pool’s own holdings and synced into reserves before the incoming tokens arrived. Run on a schedule against the chain, it surfaces the violation before a pool is emptied.