# Security Gauntlet — Progress Report

**Status: ONGOING. This is not a third-party audit and no third-party audit
of these contracts exists.**

ANANSI deployed to Base mainnet on 2026-09-09 while this work was, and remains,
incomplete. That was a deliberate decision taken with the gaps below known and
written down, not a claim that the gaps were closed. The **WHAT THIS DOES NOT
COVER** section at the end is the honest state of the work and is longer than
the covered list.

Deployed addresses, all source-verified on BaseScan:

- Token `0x4e50a097b37Fb3949733Ce9f7356500b9cc9A702`
- POL escrow `0x5290D992439C793241E30Ebd0ec464dB014D3e08`
- Burn engine `0x2Ac70DB94f71dF655d2c4210D74C18091d87a7D8`

Scope: `HardFloorToken`, `MultiVenueBurnEngine`, `RevenueRouter`,
`RevenueSplitter`, `POLEscrow`, `BurnFeeHook` (+ `BurnFeeHookDecay`, unused).

This document is published in full, including the parts that make us look
bad, because a report that only contains reassuring results is not evidence
of anything.

---

## Defence-in-depth can HIDE defects from mutation testing

A mutation score is systematically OPTIMISTIC wherever a `try/catch` wraps a
call. Concretely: the R-01 fix added a `try/catch` around `quoteV2` inside
`quoteBestV2`, so that no single bad venue could abort the loop and brick every
buyback path. That protection is correct and stays. But it also means a
loop-bound mutant — `i < n` becoming `i <= n`, which reads `venues[n]` out of
bounds — SURVIVES: the out-of-bounds revert is caught and the iteration simply
skipped. The defect is real; the harness cannot see it.

The general form: any defect whose only symptom is a revert becomes invisible
to mutation testing once something upstream swallows reverts by design. Layers
that make the system safer make the measurement weaker, and the two pull in
opposite directions.

This is not an argument against the `try/catch` — an unfixable permanent DoS
is far worse than a blind spot. It is an argument for knowing where the blind
spots are, so a high score is not mistaken for coverage it does not have.
`test/mutate.py` now reports this limitation in its own output.

## Documents get the same review cadence as contracts

A round of independent review found FOUR documents had drifted while the code
improved -- EPOCH_BUDGET.md still told a reader that same-transaction
manipulation was a live unmitigated vector after the F-09 TWAP shipped, and
still cited a deploy default that had already been fixed. That misleads in
both directions at once: under-reporting a protection while over-reporting a
risk.

The code is reviewed every round. The documents were not, and they are what a
prospective holder actually reads. They are now in scope for every review,
and any evidence change updates the affected document in the SAME commit.

## Prohibited claims

This report does not claim, and no marketing may claim, that these contracts
are bug-free, audited, safe, or cannot be hacked. It states what was run,
what was found, and — in the final section — what was not covered at all.
The uncovered list is currently much longer than the covered one.

---

## A conflict you should weigh

**The author of this report wrote most of the contracts and most of the
tests under review.** Step 0 of the gauntlet asks for an independent
re-derivation of invariants *before* reading the test suite. That was not
available here: the same author had already written both. The mitigation was
to derive invariants systematically from contract text and to actively hunt
for claims the code does not honour — which is how G-01 below was found. It
is not a substitute for a reviewer who did not write the code, and the two
findings so far were both self-inflicted, which is precisely the argument for
an outside reader.

---

## Findings

### G-01 — `POLEscrow.totalNotified` was caller-inflatable, and its comment said otherwise
**Severity: low technically, high for credibility. Status: FIXED (removed).**

The contract exposed:

```solidity
uint256 public totalNotified;
function notifyDeposit(address token, uint256 amount) external {
    totalNotified += amount;
    emit Received(msg.sender, token, amount);
}
```

Unauthenticated, and it added a **caller-supplied** number. Its own docstring
claimed it *"reads the actual balance; cannot be inflated by lying callers
beyond what the token contract reports."* No balance was ever read. Anyone
could call `notifyDeposit(anything, 2**200)` and set the counter to whatever
they liked.

Funds were never at risk — the escrow still has no exit path. The damage
would have been to reporting: any dashboard or marketing surface showing
`totalNotified` as "protocol-owned reserves" would have displayed a number an
attacker chose. For a project whose stated differentiator is that every
published number is verifiable, shipping a poisonable counter would have been
self-inflicted.

**Disposition:** removed rather than repaired. `held(token)` reads the real
balance from the asset itself, which is the only figure that can be trusted.
A stored mirror of a live value is pure liability in a contract that can never
be fixed after deploy.

### G-02 — The test suite asserted the bug was correct behaviour
**Severity: process. Status: FIXED.**

`test_escrow_has_no_exit_path` called `notifyDeposit(usdc, 5_000e6)` and then
asserted `totalNotified == 5_000e6`. It confirmed the inflatable counter
worked instead of catching that it could be inflated. The suite was green
throughout.

This is the clearest possible argument for the gauntlet's mutation-testing
requirement: **a passing suite proves the tests agree with the code, not that
the code is right.** The test now asserts the invariant that matters — that
reported holdings equal real balances, that a third party cannot change what
the escrow reports, and that balances only move in.

That requirement has since been carried out, and it found twelve more places
where the suite was not watching. See G-06.

### G-03 — Routing hook fees to the Splitter (F2 as specified) would strand them permanently
**Severity: would be critical if deployed. Status: NOT IMPLEMENTED — caught at design time.**

The gauntlet's F2 asks that hook fees route to `RevenueSplitter` so swap fees
participate in the 55/20/25 split. They cannot, as built:

- `RevenueSplitter` is **USDC-only**: `IERC20 public immutable usdc`, and
  `distribute()` reads `usdc.balanceOf(address(this))` and transfers only USDC.
- It has **no rescue path of any kind** (verified: the only matches for
  rescue/withdraw/sweep/owner in the file are comments).
- Hook fees arrive in the **pool's** currencies. For an ANANSI/WETH pool that
  is WETH or ANANSI — never USDC.

So routing hook fees there would send assets into an immutable, ownerless
contract that cannot distribute them and cannot release them. **Permanently
lost, with no recovery for anyone.**

F2 was therefore not implemented. Options, none yet chosen:
(a) leave hook fees routing to the engine (current behaviour — 100% burn, safe,
but swap fees do not join the split);
(b) convert fees to USDC before the splitter — adds a swap to the money path
and with it slippage and new attack surface;
(c) a multi-asset splitter — more code in the least-fixable place.

The cleanest disclosure may simply be that the 55/20/25 split applies to
**service revenue** (which genuinely is USDC) and not to swap fees.

### G-04 — Renouncing ownership permanently disables both rescue functions
**Severity: medium, inherent to the design. Status: DOCUMENTED, unresolved.**

`RevenueRouter.rescueToken` and `MultiVenueBurnEngine.rescueToken` are both
`onlyOwner`. The two-phase launch ends with `renounceOwnership()`, after which
`owner()` is the zero address and **both functions become permanently
uncallable**.

Consequence: any foreign token sent to the router or the engine *after*
renouncement is unrecoverable by anyone, forever. This is the deliberate
trade-off of renouncing — the same property that stops an owner draining the
contracts also stops anyone undoing a mistake. It should be stated plainly
rather than discovered by a user who misdirects a transfer.

### G-05 — Engine ETH is unspendable if no venue is usable post-renounce
**Severity: medium. Status: DOCUMENTED, unresolved.**

The engine has **no ETH withdrawal function at all** — by design, ETH in is
buyback-only. Its only outbound path is a swap through a registered venue.
Venue registration (`addVenue`, `setVenueEnabled`, `setV4Pool`) is `onlyOwner`.

After renouncement, the venue set is frozen. If every registered venue later
becomes unusable — pool drained, pair dead, v4 pool migrated — then ETH held
by the engine has no path out. **UPDATE: partially resolved.** `addCanonicalVenue` now allows anyone to register a canonical pool permissionlessly, for the life of the contracts, so the venue SET no longer freezes at renouncement -- only the venue TYPES do (see Permanent limitations). Note that this fix itself shipped with R-01, a permanent denial of service, because it validated the pool address but not the caller-supplied fee. What remains true is that if every registerable venue type becomes unusable, engine ETH would sit
there permanently.

This is not a bug in the code; it is a consequence of combining "no withdrawal"
with "no owner". It deserves an explicit decision before renouncing: either
accept it, or register venues that are highly unlikely to die.

---

### G-06 — Mutation testing found twelve guards and branches that no test was watching
**Severity: medium (test quality, not contract behaviour). Status: FIXED.**

G-02 showed that a green suite proves the tests agree with the code, not that
the code is right. Mutation testing is the mechanical version of that check:
break the contract on purpose, one edit at a time, and see whether any test
objects. A mutant that survives is a behaviour that could change in production
with nothing to catch it.

**First campaign: 61/77 killed (79.2%), 16 survivors.** Per contract:
RevenueSplitter 19/20, POLEscrow 1/1, HardFloorToken 7/11, RevenueRouter 34/45.

Twelve of the sixteen were genuine blind spots. Per the gauntlet rule — *fix
the test, not the mutant* — no contract code was changed. 24 tests were added
in `test/MutationGaps.t.sol`, each naming the mutation it exists to kill. The
notable ones:

- **The entire bootstrap phase was untested.** Every latch test funded
  `POL_TARGET` in a single distribution, so "latches when cumulative POL
  reaches the target" and "latches on the first distribution ever" were
  indistinguishable. Changing `&&` to `||` — which ends the bootstrap phase
  after one payment and cuts POL funding from 20% to 5% forever — passed the
  whole suite. Now pinned by an exact biconditional:
  `latched == (cumulativePol >= POL_TARGET)` after every distribution.
- **The slippage floor had no test.** Deleting `if (out < minEthOut) revert
  ZeroAmount();` from `convert()` was not noticed by any test. The suite
  checked that conversion works, never that its guards fire.
- **Both `EngineRejectedEth` checks had no test.** Deleting either one — so a
  failed ETH send to the engine is silently swallowed and the revenue is
  counted as forwarded anyway — passed.
- **Half the pair validation carried no test weight.** In
  `(t0 == tokenIn && t1 == weth) || (t0 == weth && t1 == tokenIn)` **(as it stood at the time; that self-report check has since been replaced by canonical-factory validation, so this quote no longer matches src/RevenueRouter.sol)**, all three
  mutations of the *first* disjunct survived: every existing test built its
  pair with address-sorted ordering, so the second disjunct always decided the
  result. Which slot the revenue token occupies depends on its address, so
  both orderings are reachable in production.
- **The supply floor's exact boundary was never deployed.** `initialSupply_ <
  FLOOR` versus `<= FLOOR` differ only at exactly the floor, and no test
  deployed there — so nothing verified that a token minted at exactly
  21,000,000 is legal.
- **Zero-address guards on the router constructor and `setRoute`, and
  `NothingToBurn`, were all deletable** without a test objecting.

**Second campaign, after the added tests: 73/77 killed (94.8%).** All four
remaining survivors are **equivalent mutants** — no input distinguishes them
from the original, so no test can kill them. Each is left in the contract and
justified in the test file rather than removed to improve a number:

| Survivor | Why it is unkillable |
|---|---|
| `RevenueSplitter:96` `toRouter > 0` → `>= 0` | `distribute()` reverts unless `bal >= 1`, and the two floored legs take at most 45% of it, so the router leg is always `>= 1`. The guard is dead code under the current constants. |
| `HardFloorToken:55` `supply > FLOOR` → `>=` | The branches differ only at `supply == FLOOR`, where both yield 0. |
| `HardFloorToken:74` `amount > headroom` → `>=` | Differ only at `amount == headroom`, where both select the same value. |
| `RevenueRouter` `if (amountIn == 0)` deleted *(line number was 147 at campaign time; the guard has since moved)* | Redundant: `amountIn == 0` implies `out == 0`, and `minEthOut >= 1` is already established, so the next line reverts with the identical `ZeroAmount` error. |

Excluding equivalent mutants, the score is 73/73. **That is a statement about
test sensitivity on four contracts, and nothing more.** It does not mean the
contracts are correct — mutation testing can only tell you the tests would
notice a change, not that the behaviour they pin down is the right one. Both
G-01 and G-02 were cases where the intended behaviour itself was wrong, and no
mutation score would have caught either.

---

## Tools run

| Tool | Version | Status | Result |
|---|---|---|---|
| Slither | 0.11.6 | RUN | 53 findings (4 High, 12 Medium, 22 Low, 15 Info) — triaged below |
| Foundry test suite | forge 1.7.1 | RUN | 86/86 passing, fuzz runs=512 |
| Aderyn | — | NOT RUN | |
| Mythril | — | NOT RUN | |
| Semgrep | — | NOT RUN | |
| Halmos | 0.3.3 | **RUN** | 3 invariants PROVEN symbolically, 1 timeout — see catalog |
| Kontrol | — | NOT RUN | |
| Echidna | — | NOT RUN | |
| Medusa | — | NOT RUN | |
| Mutation testing (`test/mutate.py`) | in-repo | **RUN** | Four-contract campaign **73/77 = 94.8%** (4 survivors, all equivalent). Seven-contract campaign is WORSE and is the number that matters: `MultiVenueBurnEngine` **62.2% -> 86.4%**, `BurnFeeHook` 76.9%. Survivors there are **NOT** all equivalent — best-venue tie-breaking and buyback delta accounting are genuine silent-wrong-answer gaps. **All scores predate the R-01..R-04 contract changes and must be re-measured.** |

### Slither triage — High impact (4)

All four are `arbitrary-send-eth` against `_sweep` / `sweepStranded` in the
two hooks.

**Disposition: false positive, with reasoning.** Both functions send ETH only
to `burnEngine`, which is declared `address public immutable burnEngine`, set
once in the constructor, and rejected if zero. There is no setter and no
other destination in either function. Slither's detector does not model
immutability as a constraint on the destination. Accepted, not silenced —
if the field ever stops being immutable this finding becomes real.

### Permanent limitations — venue types freeze at deploy

Stated here rather than in a footnote, because it is irreversible and a buyer
cannot discover it from the code without reading four contracts together.

**Frozen: venue TYPES.** Pool validation is performed against factory
addresses hardcoded in `BaseFactories` — Uniswap v2, Uniswap v3, the v4
PoolManager, and Aerodrome, all on Base. Those constants cannot change after
deployment, and `addVenue` is owner-only and therefore dead once ownership is
renounced. **A venue type that does not exist today can never be added.** If
Uniswap ships a v5, this system cannot use it, ever. `RevenueRouter`'s engine
address is immutable too, so the pipeline cannot be re-pointed at a
newly-deployed engine as a workaround. There is no upgrade path and no
governance switch, by design.

**Not frozen: POOLS.** Within those four venue types, new pools remain
permissionlessly registerable forever. Anyone can register any pool the
canonical factory confirms it created, without permission from us and without
an owner key existing. A deeper v3 pool at a different fee tier, a new
Aerodrome pool, a replacement v2 pair — all remain addable by any caller for
the life of the contracts.

So the correct summary is: **the set of venue TYPES is fixed at deploy; the set
of POOLS is open forever.**

Why hardcoding was chosen over a configurable factory address: a constructor
parameter would let a careless or compromised deployer aim validation at a
factory of their own, which reintroduces exactly the vulnerability the
validation exists to close (F-04). The freeze is the price of removing that
key, and it is a price we chose knowingly.

What makes the trade defensible rather than merely accepted: immutable AMMs do
not decay. Uniswap v2 launched in 2020 and still holds real liquidity today.
Being limited to v2/v3/v4/Aerodrome is a ceiling on future options, not a path
to the system becoming unusable. We could be wrong about that, and if we are,
there is no remedy — which is the whole reason it is disclosed here.

### Slither triage — Medium impact (12)

- **`locked-ether` on POLEscrow — TRUE, INTENTIONAL, and disclosed.** ETH
  sent to the escrow is permanently unrecoverable by anyone. That is the
  documented v1 design (deposit-only accumulator, no withdrawal path, founder
  has zero access). Slither is correct and this is the trade we chose. It is
  disclosed publicly on the site, not just here.
- **`incorrect-equality` (8 instances)** — all are `== 0` guards on balances
  or amounts (`if (bal == 0) revert`). Strict equality against zero is the
  intended semantics. Accepted.
- **`unused-return` (2)** — `getReserves()` returns a third value (the block
  timestamp) that we deliberately ignore. Accepted.
- Remaining items are style/informational.

**Not yet done:** the Low (22) and Informational (15) findings have not been
individually triaged.

---

## Invariant catalog — proof status

Derived from contract text. **"Proven" means symbolically proven by Halmos
0.3.3, for amounts bounded to uint64 — not for the full uint256 range.**
I-3 and I-6 are proven on that basis. **I-5 no longer applies to this code at all** - the latch it covered was deleted. I-4 is NOT proven: it times out, and a
timeout is not a proof. Everything else rests on bounded fuzzing.

(This header previously read "Nothing is yet proven" while sitting four lines
above three rows marked PROVEN. Caught by an independent reviewer, not by us; see the fresh-session findings F-01..F-13 and R-01..R-04 below.)

| # | Invariant | Status |
|---|---|---|
| I-1 | Total supply can never fall below 21,000,000 FLOOR | fuzzed only |
| I-2 | No mint path exists after deploy | unit-tested |
| I-3 | Splitter conserves value exactly: in == burn + POL + operator | **PROVEN** (Halmos, 37 paths, amounts < 2^64) |
| I-4 | Rounding dust always favours the burn path | fuzzed only — **symbolic run TIMED OUT at 69 paths** |
| I-5 | ~~The $50k phase latch is one-way~~ | **RETIRED - NOT PROVEN OF CURRENT CODE.** The latch this covered was DELETED in the three-phase rewrite. Deleting it retires the PROPERTY, not just the proof. `phase()` is a different one-way mechanism. NOTE 2026-08-30: it is now the supply floor ALONE -- `totalSupply() > SUPPLY_FLOOR ? 1 : 2`. The cumulative-ANANSI-to-POL cap named here was deleted with phase 3 (dcf19b4); this row previously described a mechanism the code no longer has. It inherits NONE of the 246-path evidence. Its proof is un-discharged and is a pre-renounce blocker. |
| I-6 | No path moves tokens or ETH to a founder-controlled address | **PROVEN** (Halmos, 41 paths, any amount < 2^64, any founder addr, any caller) |
| I-7 | Hook fee is always exactly 200 or 100 bps, never other | not implemented yet (see below) |
| I-8 | Engine has no token exit except burn | unit-tested, not proven |
| I-9 | Post-renounce, every privileged setter reverts | unit-tested on mocks, **not on a fork** |
| I-10 | Escrow reported holdings == real balances | **newly tested (G-01/G-02)** |

**I-6 is now proven, not asserted.** Over symbolic inputs — any amount below
2^64, any founder address that is not one of the three constructor-fixed
destinations, and any caller — no call sequence to `distribute()` moves value
to that address. This was previously only claimed by reading the code.

**Bounds are part of the claim.** Amounts are constrained to 2^64 (about 18
trillion USDC at 6 decimals). The proof holds for every value up to that
bound, not for all uint256. An unbounded run timed out at 77 paths, and a
timeout is not a proof.

**I-4 (dust favours burn) remains UNPROVEN.** The first formulation asserted
`toRouter * 10_000 >= amount * 5_500`, which multiplies two symbolic values;
nonlinear arithmetic is where SMT solvers fall over and it timed out at 196s.
Restating conservation linearly dropped it from a timeout to a 0.92s proof —
but the dust property still times out at 69 paths even reformulated. It is
covered by fuzzing only. This is a genuine gap, not a formality: dust
direction is the mechanism that guarantees rounding never favours the
operator over the burn path.

---

## Not implemented yet

**F1–F4 (the 200bps→100bps one-way fee step at 365 days) is NOT BUILT.**
The current `BurnFeeHook` is a flat immutable fee. `BurnFeeHookDecay` exists
but implements a linear decay whose duration is an UNBOUNDED constructor parameter — not a short window, and not a one-way step at a
year, and it is not deployed. Fee routing currently targets the burn engine
directly, **not** the RevenueSplitter, so the 55/20/25 split (and the
disclosure that 25% of swap fees go to the operator LLC) does not yet apply
to hook fees.

---

## WHAT THIS DOES NOT COVER

Everything below is untested. This list is the honest state of the work.

- **Symbolic proofs are partial.** Halmos 0.3.3 HAS been run: I-3 and
  I-6 are proven for amounts bounded to uint64. Kontrol has not been run, and
  **I-4 (dust favours burn) remains UNPROVEN** -- it times out, and a timeout
  is not a proof. Every other invariant in the catalog rests on bounded
  fuzzing at 512 runs, not on proof.
  (This bullet previously said Halmos had not been run and that nothing was
  proven. That was left stale after the Halmos runs and directly contradicted
  both the tools table and the invariant catalog in this same document. It was
  caught by an independent reviewer, not by us; see the fresh-session findings F-01..F-13 and R-01..R-04 below.)
- **Mutation testing now covers seven contracts, with uneven results.**
  `MultiVenueBurnEngine` first scored 62.2% (34 survivors, almost all
  unprovoked guards) and 86.4% after remediation. `BurnFeeHook` 76.9%,
  `FounderVesting` 100%. Survivors remain, including best-venue tie-breaking
  and buyback delta accounting -- both silent-wrong-answer bugs rather than
  guards, which is why guard remediation did not reach them. The operator set is also finite — arithmetic,
  relational, equality, boolean, and guard deletion — so it does not model
  reordered statements, swapped arguments, or wrong-variable substitutions.
  A 94.8% score on four contracts is not a statement about the other three.
- **No forked-mainnet testing.** Nothing has been run against real
  PoolManager, real USDC, or real pools. Every adversarial scenario in the
  gauntlet — flash-loan quote manipulation, keeper sandwiching, PoolManager
  reentrancy, v4 delta sign errors, donation attacks, epoch-cap bypass,
  front-running the latch crossing — is **untested**.
- **No quantified keeper-compromise loss bound.** We assert the epoch cap
  bounds it; we have not proven a number.
- **Fund-loss surfaces now enumerated (G-03/G-04/G-05 above), but NOT
  exhaustively tested.** Known permanent-loss surfaces: anything sent to
  POLEscrow (by design); non-USDC assets sent to the Splitter; foreign tokens
  sent to router/engine after renouncement; engine ETH if all venues die
  post-renouncement. None of these are code defects — all are consequences of
  immutability and renouncement — but every one destroys value silently.
- **No systemic dependency analysis.** USDC can pause and can blacklist
  addresses. Our router and splitter are immutable with no rescue. If USDC
  blacklists the splitter, funds routed there are frozen permanently and
  there is no admin path to recover them — this is believed true and has not
  been modelled or tested. Same for PoolManager pause/upgrade and WETH.
- **No bytecode/immutability proof.** No decompilation, no proof of the
  absence of DELEGATECALL / SELFDESTRUCT / CREATE2, no storage-layout audit.
- **No compiler-risk review.** We compile with `viaIR` and have not reviewed
  solc 0.8.26 known-bug lists or compared viaIR vs non-viaIR behaviour.
- **No differential testing** against a canonical OZ ERC-20 reference.
- **No weird-token handling tests** (fee-on-transfer, rebasing, ERC-777
  callbacks, non-standard returns, non-18 decimals).
- **No access-control matrix.**
- **No economic simulation or chaos injection.**
- **No third-party scanner submissions** (GoPlus, TokenSniffer, De.Fi,
  honeypot.is).
- **No soak.** Zero days of the required 14-day Sepolia soak have run.
- **No external review.** Every finding so far was found by the person who
  wrote the code.

---

*Six findings G-01..G-06 were self-inflicted and found in-house. Two later independent reviews then found 13 more (F-01..F-13) and 4 blocking issues (R-01..R-04), including a permissionless permanent denial of service we had introduced while fixing G-05. The in-house count was never the whole picture, and the outside reader found the worst item. Everything below started from asking "what does
this claim that the code does not do?" That question has not yet been asked
of most of the codebase.*