This section contains assertion patterns organized by use case categories.

Comprehensive Protocol Suites

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.

Access Control & Administrative Changes

  • 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.

Liquidity Pool & AMM Security

  • 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 Protocol Safety

  • 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 Security

  • 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.

Vault & ERC4626 Security

  • 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.

Emergency & Special Mode Protection

  • Panic State Validation: Validates critical protocol state variables during panic or emergency modes, ensuring fallback mechanisms work correctly when normal operations are suspended.

Data Integrity & Message Verification

  • Farcaster Protocol Integrity: Ensures the integrity of cross-chain messages in the Farcaster protocol, preventing unauthorized or malformed message processing.

Fund Protection

  • 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.