This is a collection of assertion suites for full protocols. These are deep dive use cases based on deployed and used protocols and a great starting point for understanding how to write assertions for your own protocols.
Aave V3 Suite: A comprehensive collection of assertions for the Aave V3 lending protocol, demonstrating real-world application of assertion patterns.
Optimism FMA Suite: Assertions based on Optimism’s Failure Mode Analysis framework, covering cross-chain message passing and bridge security.
Implementation Address Change: Protects against unauthorized changes to proxy implementation addresses, preventing attackers from replacing contract logic with malicious code.
Owner Change: Ensures ownership of a contract cannot be transferred unexpectedly, preventing attackers from gaining administrative control over critical protocol functions.
Timelock Verification: Verifies that administrative actions are executed only after the required timelock period, preventing rushed or malicious changes to protocol parameters.
Constant Product: Ensures the constant product formula (k = x * y) is maintained in AMM pools, preventing price manipulation attacks and unauthorized token drains.
Price Within Ticks: Verifies that concentrated liquidity positions in AMM protocols maintain prices within expected tick boundaries, protecting against price manipulation.
Fee Calculations: Ensures trading fees are correctly calculated and distributed, preventing fee theft or unexpected losses in AMM protocols.
Lending Health Factor: Enforces minimum health factor requirements in lending protocols, preventing under-collateralized positions and protecting protocol solvency.
Liquidation Health Factor: Ensures liquidations only occur when health factors fall below the liquidation threshold, protecting borrowers from premature or incorrect liquidations.
Sum of All Positions: Verifies that the sum of all user positions matches the total asset balance, detecting accounting errors or unauthorized fund movements.
Tokens Borrowed Invariant: Enforces that the relationship between borrowed tokens and collateral remains within safe protocol limits, preventing critical invariant violations.
Oracle Liveness Validation: Verifies that oracle data is fresh and updated within an acceptable time window, preventing the use of stale or manipulated price data.
TWAP Deviation: Ensures the time-weighted average price doesn’t deviate excessively from previous values, detecting price manipulation attempts or oracle failures.
Intra-Transaction Oracle Deviation: Monitors price oracle readings during a transaction to detect excessive deviations that might indicate flash loan attacks or price manipulation.
ERC4626 Assets to Shares: Verifies correct conversion between assets and shares in ERC4626 vaults, preventing accounting errors that could lead to fund loss.
ERC4626 Deposit and Withdraw: Ensures deposit and withdrawal operations maintain correct accounting in ERC4626 vaults, protecting user funds during transfers.
Harvest Increases Balance: Verifies that yield-generating operations like harvests always increase the total balance of vaults, preventing value extraction attacks.
Panic State Validation: Validates critical protocol state variables during panic or emergency modes, ensuring fallback mechanisms work correctly when normal operations are suspended.
Farcaster Protocol Integrity: Ensures the integrity of cross-chain messages in the Farcaster protocol, preventing unauthorized or malformed message processing.
ERC20 Drain: Prevents excessive token outflows in a single transaction, mitigating the impact of potential exploits by limiting how quickly funds can be drained.
Ether Drain: Monitors and limits ETH outflows from contracts, protecting against unauthorized withdrawals that could deplete protocol reserves.
Next: Explore previous hacks analysis to see how assertions could have prevented real-world exploits.