Defi Invariant Check

<!-- inspired by trailofbits/skills (concept); repointed to native CLIs for Chrono -->

defi-invariant-check

DeFi-specific invariant authoring and testing discipline. Use this as a sub-skill during evm-audit-flow when the target is a DeFi protocol (AMM, lending, yield, bridge, stablecoin, perps). Generic Echidna/Medusa campaigns miss DeFi-specific invariants — this skill provides the property checklist. All tools are the native host CLIs (echidna, medusa, forge, halmos) run in the target project directory; there is no wrapper layer.

Invariant categories

Token accounting invariants (always required):

• totalSupply == sum(balanceOf(all_holders)) — no spurious minting or burning.
• reserve0 * reserve1 >= k (for constant-product AMMs) — k-invariant never decreases except via fee accrual.
• totalBorrow <= totalDeposit for all lending pools — protocol cannot lend out more than deposited.
• sum(userShares) == totalShares for yield vaults — share accounting is consistent.

Access-control invariants:

• Only authorized roles can set oracle addresses, fee parameters, or pause state.
• onlyOwner/onlyGovernance functions cannot be called by arbitrary external accounts.
• Upgradeable proxy implementation slots cannot be modified except through the upgrade pathway.

Economic/oracle invariants:

• Flash loan callbacks cannot leave the protocol in a net-loss state after the loan repayment.
• Liquidation proceeds must cover the borrowed amount plus protocol fee — no bad-debt accrual from liquidations.

2026 incident-derived oracle-input robustness invariants (highest-priority economic class):

• Spot versus TWAP: a price used for collateral, borrowing, liquidation, minting, or redemption must reject or clamp a same-block spot price when abs(spot - TWAP) / TWAP > maxDeviation; no value-affecting path may silently fall back to the divergent spot. This targets the oracle/valuation-manipulation class represented by Moonwell (2026-08-27), Lazy Summer (2026-07-06), Makina (2026-01-20), and Edel (2026-07-01) in V114-51.
• Low-liquidity collateral: within the protocol's configured manipulation budget, an atomic trade against a thin market cannot increase an account's borrowable value or liquidation proceeds by more than the attacker's net cost plus the configured safety margin. Reject collateral whose observable depth cannot support the valuation notional. This is the Moonwell low-liquidity-collateral oracle shape from V114-51.
• NAV manipulation bound: absent external profit or loss, a deposit/reprice/redeem round trip across any supported asset must not return more value than entered after fees and rounding tolerance, and one manipulable component price must not move total NAV beyond its configured exposure and deviation caps. This targets the Lazy Summer, Makina, and Edel valuation/NAV incident class from V114-51.

2026 incident-derived governance/timelock invariants (second priority):

• Delay cannot be bypassed or shortened: for every queued privileged operation, executedAt - queuedAt >= max(delayAtQueue, protocolMinimumDelay). Changing the delay, executor, proposer, or role graph after queueing cannot accelerate that operation, and a delay change itself becomes effective only after the pre-change delay. This targets Term Finance's 2026-08-24 timelock-zeroing shape from V114-51.
• A role or executor change cannot authorize its own proposal or execution; every privilege expansion must be queued and executed by the pre-change authority after the full pre-change delay. Snapshot the audited role graph and assert that no post-deployment role drift broadens value-moving authority outside that path. This targets the TOP (2026-06-26) and BonkDAO (2026-07-26) governance-bypass shapes from V114-51.

Rounding/precision invariants (third priority, still required):

• Exercise zero-supply initialization, one-unit deposits/withdrawals, values immediately below and above every division boundary, and repeated dust operations. No non-zero asset input may mint zero shares unless the transaction reverts or the loss is explicitly bounded; no positive supply or assets may exist without corresponding claimable shares.
• A deposit/redeem or mint/withdraw round trip, with no external profit or loss, must return the starting economic value within the documented fee and rounding bound; splitting one operation into many dust-sized operations cannot improve that bound.
• Fuzz solver domains and every fixed-point math-library boundary used by share conversion, including zero denominators, scale changes, and minimum/maximum supported values. These properties retain the dust/zero-supply class seen twice at Thetanuts in June 2026, while placing it behind the two larger 2026 code-level classes identified by V114-51.

Reentrancy invariants:

• Protocol state (balances, reserves, shares) after any external call must equal the state written before the call (CEI pattern verification).
• No re-entrant call can increase the caller's balance beyond their pre-call entitlement.