Aave V3 Suite

We’ve taken a deep dive into the Aave V3 protocol and have created a suite of assertions that can be used to increase the security of the protocol.

In general, the Aave V3 smart contracts are very well written and follow best practices with regard to security. We chose Aave V3 because it’s a popular and battle-tested protocol that would serve as a good case study for writing real-world assertions.

Link to the Phylax fork of Aave V3: https://github.com/phylaxsystems/aave-v3-origin/tree/feat/assertions

​

Approach

One of the most common ways of writing assertions is by expressing the protocol invariants as assertions.

Aave V3 has put a lot of effort into invariants, as can be seen in the Aave V3 Invariants documentation. Specifically, the invariants specification was helpful for writing assertions, and most of the assertions we wrote are based on the invariants.

We have mocked parts of the protocol in order to properly test the assertions and ensure that they only revert transactions that break the invariants. The mocks are located in the mocks directory.

​

Here Be Dragons

In order to showcase the real power of assertions, we have introduced a bug in the protocol.

Anyone borrowing exactly 333e6 tokens will receive double the amount of tokens they would normally receive if they borrowed any other amount.

The bug can be found in the BorrowLogic.sol file.

​

Assertion Collections Overview

• BaseInvariants - Core protocol invariants for debt token supply validation, ensuring the sum of individual user debt balances matches the total debt token supply for specific assets.

• BorrowLogicErrorAssertion - Validates that borrow amounts correctly match underlying token balance changes, ensuring users receive the exact amount they borrowed.

• BorrowingInvariantAssertions - Comprehensive borrowing post-condition checks including liability decreases, health factor validation, reserve state verification, borrow caps, and balance/debt change tracking.

• FlashloanInvariantAssertions - Ensures flash loans are properly repaid with sufficient funds (amount + fee) returned to the protocol.

• HealthFactorAssertions - Validates health factor invariants across all operations, ensuring healthy accounts don’t become unhealthy, proper actor isolation, and correct health factor transitions for different action types.

• LendingInvariantAssertions - Supply and withdrawal post-condition checks including reserve state validation, supply caps, balance change verification, and collateral withdrawal health requirements.

• LiquidationInvariantAssertions - Liquidation-specific invariants covering health factor thresholds, grace periods, close factor conditions, deficit creation/accounting, and reserve state requirements.

• OracleAssertions - Price oracle validation including maximum price deviation checks (5%) and price consistency verification across transactions.

Each collection focuses on specific protocol operations and ensures critical invariants are maintained during Aave V3’s core lending, borrowing, and liquidation functions.