Protocol Invariants: AMM, Lending and ERC4626 Properties Auditors Can Check

Why invariants

A test can call every public function and still miss the property that makes the protocol economically coherent. Coverage describes which code the test reached. Protocol invariants describe the relationships that should remain true across allowed transitions. The two forms of evidence answer different questions.

Write a property with its assumptions. An assertion that a vault never loses assets is wrong for a strategy that can realize investment losses. A more useful property might require that reported losses are reflected in the accounting and cannot be shifted to an unrelated user through a rounding or timing defect. The specification must say which behavior is legitimate before the test can distinguish a failure.

A stateful campaign generates sequences. Depositing after a donation can expose a different condition from depositing into a new vault, and liquidating after a price change can differ from borrowing under the same price. The handler and state model determine which sequences the campaign can reach.

Foundry's invariant-testing documentation describes target contracts and handler patterns. It also provides metrics for understanding calls and discarded or reverting inputs. Read those observations alongside the assertion result. A campaign in which meaningful actions continually revert may preserve an invariant without exercising the operation the team wanted to test.

An auditor should be able to connect each important property to the business rule it protects and the actions that can threaten it. The threat model supplies the actor and trust assumptions. The invariant suite turns selected assumptions into checks that can run against a concrete implementation.

The vault interface contains more observations than actions

Method

Source and selection

Every function declared directly in OpenZeppelin IERC4626.sol v5.4.0. Exclude inherited ERC20 declarations and events. Classify external view versus state-changing and function-name families.

Retrieved

2026-09-05

Observation

Every function directly declared in IERC4626.sol at OpenZeppelin Contracts v5.4.0; inherited ERC20 functions and events were excluded.

Results

The interface declares 16 functions: 12 views and 4 state-changing operations. This asymmetry is useful when designing a harness. Testing only deposit and withdrawal transitions leaves much of the externally observable contract unexamined.

The function names do not prove behavioral compliance. They identify the observations that a test model should relate to the corresponding actions. A preview can be present and still quote the wrong rounding direction; a maximum function can return a value that does not reflect the intended operational limit. Those relationships require assertions against actual behavior.

Limits

• This is a static interface classification. No vault implementation was executed by the census.
• Inherited token operations matter to a complete harness but are outside this direct-declaration denominator.
• The family labels describe function roles; the standard and implementation determine the precise conditions of each assertion.

The reproducible record is kept in the repository: seo/research/articles-32-41-2026-09-05/surveys.py and seo/research/articles-32-41-2026-09-05/survey-38.json. These file paths are not public downloads.

AMM invariants

An automated market maker needs properties that reflect its specific pricing and fee rules. Do not copy a constant-product assertion into every pool design. Concentrated-liquidity systems, stable-swap curves and weighted pools have different state models, and an invariant meaningful for one can be false or incomplete for another.

The Uniswap V2 pair source provides a concrete reference. Its swap path checks a product relationship using fee-adjusted balances. That is more precise than saying that reserves must always multiply to the same number. Fees, liquidity changes and direct token transfers mean the raw product need not remain constant across every action.

Model reserve synchronization separately from user swaps. A token transfer into the pair changes balances before a reserve update necessarily occurs. An assertion that balances always equal stored reserves would reject an allowed intermediate situation. Choose the observation point at which the protocol promises the relationship.

Include actor diversity in the harness. A property that passes when the same test address provides liquidity and swaps may fail to exercise another user's claims. Track balances for the actor set and document how accounts outside that set are handled. If a callback exists, the model should identify the allowed callback behavior and the state visible during it.

A failed invariant should produce a meaningful trace. Preserve the action sequence, initial state and observed deviation from the intended rule. The reviewer needs to understand whether the failure is a protocol defect or a harness assumption that excluded a legitimate donation, fee or asset behavior.

The reentrancy analysis is relevant when an external interaction exposes intermediate accounting. The useful assertion identifies the value relationship or authority that must survive the callback; naming reentrancy without a protected property leaves the test's purpose unclear.

Lending invariants

Lending systems require separate properties for opening risk, marking risk and resolving risk. An assertion that every account always has a healthy collateral ratio is usually wrong once prices can move. A price change can make an existing position liquidatable without any unauthorized borrowing.

Aave's documentation describes health factor as part of the liquidation decision. That is a mechanism to model, not a reason to assume the system prevents every unhealthy state. The harness should distinguish a user action that creates prohibited debt from an external price movement that activates a liquidation path.

Start with origination. Under the supported price and configuration assumptions, a successful borrow should satisfy the protocol's required collateral and cap checks at that transition. Then test liquidation and repayment under the conditions the protocol permits. A repayment path that becomes unavailable at the moment of distress can matter even when origination checks are correct.

Interest accrual changes the denominator of several relationships. Decide whether the test model uses principal, indexed debt or current debt and use that definition consistently. A ledger that mixes them can report a false accounting failure or conceal a real one through compensating errors.

Liquidation tests also need economically meaningful assets and prices. If the handler always clamps inputs to a narrow healthy range, it may never reach the distress states that matter. Record which price changes and liquidity constraints the model can express. Passing results should be described with that boundary.

End a lending failure investigation with the exact transition that violated the specification. A final unhealthy balance is not enough to identify a defect unless the model also explains why that balance should have been impossible under the preceding authorized actions and external conditions.

Vault invariants

An ERC4626 vault exposes several related observations rather than one universal share price. Idealized conversion functions, operation previews and maximum functions answer different questions. The standard's distinctions should remain visible in the test model.

The preview relationships are directional. Subject to the standard's conditions and the same transaction state, a deposit should not return fewer shares than its preview; a mint should not require more assets than its preview. Withdrawal and redemption have their corresponding directions. Fees and rounding are why a loose equality assertion can be the wrong test.

Do not use preview success as proof that an operation is currently permitted. Maximum functions and previews have different duties. A preview may quote an operation while an operational limit prevents it. Include tests that compare limits with the behavior they are meant to constrain rather than assuming every quote is executable.

Donations deserve a separate action in the harness. A direct asset transfer can alter the relationship between asset balances and shares without minting shares. OpenZeppelin's ERC4626 documentation explains the rounding and inflation-attack context and its virtual-offset approach. The correct test depends on the implementation being assessed, including any overrides or supported asset constraints.

1. Record shares, managed assets, fees and operational limits.
2. Read the relevant conversion, maximum or preview for that state.
3. Execute an operation under the stated account and dependency assumptions.
4. Check the required directional quote and accounting relationships.

Model strategy gains and losses explicitly. If the application reports assets through an external strategy, a simple token-balance equality may not describe its accounting. Write down which assets are managed, which are immediately liquid and how a reported loss affects claims. A test that excludes losses cannot establish how the system treats them.

Use small amounts and boundary states deliberately when they are supported. Rounding often becomes visible near those boundaries, but a failing tiny-amount operation may also be explicitly permitted by the specification. Interpret the trace against the intended behavior rather than treating every revert as either a bug or an acceptable discard.

Writing handlers auditors reuse

A reusable handler is a model with visible assumptions. It should identify the actors, target contracts, available actions and limits imposed on generated inputs. Auditors need to know what the campaign could have tried before interpreting the absence of a counterexample.

With those assumptions recorded, compare stateful fuzzing tools by the inputs and evidence your harness needs to retain.

Keep model bookkeeping distinct from the contract state being checked. A ghost variable can track an expected relationship, but updating it by copying the same potentially wrong implementation logic defeats the comparison. Explain which observations come from the contract and which quantities the harness calculates independently.

1. Define the actor set and the authority available to each role. Include privileged changes only when they are inside the intended test scope.
2. List the actions and state transitions the handler can generate, including dependency changes that the model intentionally supports.
3. Record input restrictions and expected reverts. Inspect metrics to confirm that meaningful actions actually execute.
4. Write assertions against the protocol specification, with units and rounding directions stated explicitly.
5. Preserve failing traces and reproduction inputs so another reviewer can distinguish an implementation defect from a model defect.

Review vacuous success before adding more runs. If an action is never called or always reverts, the relevant property may not have been challenged. Foundry's handler metrics can help reveal that situation. A larger number of generated inputs does not repair a model that excludes the states the assertion is intended to cover.

Provide the auditor with the suite, configuration and known modeling limits. Our Pharos Production profile and member directory help locate reviewers, but the acceptance discussion should concern the actual artifacts. Ask which properties the engagement will assess and whether the reviewer will evaluate the harness itself.

The final acceptance condition is specific: the important relationships have an understandable specification, the handler can reach the relevant transitions and counterexamples can be reproduced. Passing a campaign adds evidence within that model. It does not prove the absence of every protocol vulnerability or eliminate the need to review assumptions that the model leaves outside.

Use a counterexample to review the model too

Imagine a vault property that compares the total value of user shares before and after a sequence. A failing trace might expose an accounting defect, but it might also reveal that the model ignored fees or used inconsistent units. Preserve the trace first. Then inspect whether the assertion expresses the intended economic relationship under the actions the handler actually generated.

The repair differs depending on that answer. If the implementation violates the agreed property, change the implementation and retain the regression trace. If the property is wrong, correct the specification and document why. Silently weakening the assertion until the run passes removes the evidence that the team needs to understand the result.

Make expected reverts explicit. An action that exceeds a supported limit can legitimately fail, while a handler that generates only impossible actions may never exercise the accounting path. Inspect which calls complete and which states become reachable. The useful question is whether the campaign challenges the intended transition, not whether the test process returns a successful exit code.

Dependency behavior belongs in the model when the property depends on it. If the supported asset set excludes fee-on-transfer tokens, record that assumption and the mechanism enforcing it. If the product intends to support a broader set, the test environment should represent the relevant behavior. A mock that always returns the convenient value can make a complex integration appear simpler than the deployed system.

Hand off a short explanation with each important assertion: what it protects, when it applies and which exclusions remain. The auditor can then assess the property and harness together. A reusable suite is one whose assumptions another engineer can inspect, not simply one that imports into a new repository without syntax errors.