This document describes the specification and verification of Aave's Vault using the Certora Prover. The work was undertaken from March 29th to June 18 2023. The latest commit reviewed and run through the Certora Prover was 23366cc. The scope of our verification includes the following contracts:

ATokenVault.sol

ATokenVaultV2.sol

The Certora Prover proved the implementation correct with respect to the formal rules written by the Certora team. During verification, the Certora Prover discovered bugs in the code which are listed in the tables below. All issues were promptly addressed. The fixes were verified to satisfy the specifications up to the limitations of the Certora Prover. The following section formally defines the high-level specifications of Aave Vault. All the rules are publicly available in the GitHub repository. Certora also performed an independent manual review of the code between March 6th and March 23rd, allocating two security researchers.