This document describes the specification and verification of Aave's rescue mission phase 1 using the Certora Prover. The work was undertaken from January 6th to January 12th. The latest commit reviewed and run through the Certora Prover was 4c59da8d. The scope of our verification was the following contracts:

AaveTokenV2.sol

LendToAaveMigrator.sol

StakedTokenV2Rev4.sol

The Certora Prover proved the implementation is correct with respect to the formal rules written by the Certora team. During the verification process, the Certora Prover alerted on several issues listed in the table below. All issues were promptly corrected, and the fixes were verified to satisfy the specifications up to the limitations of the Certora Prover. The next section formally defines high-level specifications of the contracts. All the rules are publically available in the Aave-rescue-mission github repository.