Invariant

A property or condition that must always hold true throughout a smart contract's execution, used as a basis for testing and formal verification.

An invariant is a condition that must always remain true regardless of what operations are performed on a smart contract. Invariant-based testing verifies that these critical properties hold under all possible scenarios—including edge cases that developers might not anticipate. Breaking an invariant indicates a bug that could lead to fund loss, unauthorized access, or protocol failure.

Understanding Invariants

Invariants define what "correct" means for a protocol:

1// Example invariants for a lending protocol:
2// 1. totalDeposits >= totalBorrows (always more collateral than debt)
3// 2. userBalance[addr] <= totalDeposits (no user has more than total)
4// 3. sum(all userBalances) == totalDeposits (accounting consistency)
5// 4. interestRate > 0 (rate never goes negative or zero)

If any operation causes these conditions to become false, the contract has a critical bug.

Types of Invariants

Global invariants: Must hold across the entire protocol state

  • Total supply equals sum of all balances
  • Contract balance covers all user deposits

User invariants: Must hold for each individual user

  • User can always withdraw their entitled funds
  • User's debt never exceeds their collateral value

Temporal invariants: Must hold across state transitions

  • Locked tokens remain locked until unlock time
  • Once finalized, state cannot be changed

Economic invariants: Ensure financial consistency

  • AMM: x * y = k (constant product)
  • Staking: rewards + principal = withdrawable amount

Invariant Testing

Fuzzing tools use invariants to find bugs:

1// Foundry invariant test example
2function invariant_totalSupplyMatchesBalances() public {
3 uint256 sumBalances = 0;
4 for (uint i = 0; i < actors.length; i++) {
5 sumBalances += token.balanceOf(actors[i]);
6 }
7 assertEq(token.totalSupply(), sumBalances);
8}

The fuzzer executes random sequences of function calls, checking the invariant after each operation. If it breaks, the fuzzer reports the sequence that caused the failure.

Invariant Testing vs Unit Testing

Unit TestingInvariant Testing
Tests specific scenariosTests properties across all scenarios
Developer anticipates casesFuzzer finds unexpected cases
"Does X work correctly?""Does the invariant always hold?"
Limited coverageExplores vast state space

Invariant testing finds bugs that unit tests miss because developers can't anticipate every edge case.

Common DeFi Invariants

DEX/AMM invariants:

  • Constant product formula maintained
  • Reserves match actual token balances
  • Fees never exceed swap amounts

Lending protocol invariants:

  • Collateral always covers debt (before liquidation)
  • Interest accrual is monotonic
  • Borrowers can repay and reclaim collateral

Staking invariants:

  • Users can withdraw their deposits
  • Rewards don't exceed allocated pool
  • Lock periods are enforced

Token invariants:

  • Total supply equals sum of balances
  • Transfers preserve total supply
  • Allowances function correctly

Breaking Invariants = Finding Bugs

When an invariant breaks, you've found a critical bug:

Example: An ERC20 token has invariant "sum of balances == totalSupply". The fuzzer finds:

  1. User A transfers to User B
  2. Due to rounding, 1 wei is lost
  3. After 1000 transfers, totalSupply > sum of balances
  4. Bug found: accounting inconsistency

Writing Good Invariants

Fundamental: Focus on properties that must never be violated Measurable: Invariants must be checkable programmatically
Exhaustive: Cover all critical aspects of protocol correctness Documented: Explain why each invariant matters

Formal Verification Connection

Formal verification mathematically proves invariants hold for all possible inputs, not just fuzzed samples. For critical protocols, formal verification provides stronger guarantees than testing alone.

Audit Considerations

Well-defined invariants help audits:

  1. Communicate intent: Invariants tell auditors what properties matter
  2. Focus review: Auditors verify code maintains stated invariants
  3. Demonstrate testing: Passing invariant tests shows rigor
  4. Find missing invariants: Auditors may identify properties you haven't considered

Invariant-based thinking is essential for secure smart contract development—it shifts focus from "did I test enough scenarios?" to "what properties must always hold?"

Need expert guidance on Invariant?

Our team at Zealynx has deep expertise in blockchain security and DeFi protocols. Whether you need an audit or consultation, we're here to help.

Get a Quote

oog
zealynx

Subscribe to Our Newsletter

Stay updated with our latest security insights and blog posts

© 2024 Zealynx