This document describes the specification and verification of an upgrade to Aave V3 into version V3.0.1 using the Certora Prover. The work was undertaken from November 17, 2022, to December 15, 2022, on commit 428e258. The new version introduces fixes that were discovered after a year of testing V3 across different networks - context. This verification project aims to enhance the existing specifications of Aave V3 core and add new properties. The scope of our specifications includes particularly the following contracts:

StableDebtToken.sol

VariableDebtToken.sol

Atoken.sol

ReserveConfiguration.sol

UserConfiguration.sol

And partial verification of:

Pool.sol

The Certora Prover proved the protocol implementation is correct with respect to formal specifications written by the Certora team. The team also performed a manual review of the contracts. The resulting specification files are available on Aave's public git repository.