This document describes the specification and verification of Aave's static aToken V3 using the Certora Prover. The work was undertaken from January 18th to March 31st, 2023. The latest commit reviewed and run through the Certora Prover was 51d46b1. The scope of our verification includes one main contract:

StaticATokenLM.sol

With one library: RayMathExplicitRounding.sol

The Certora Prover proved the implementation is correct with respect to the formal specification written by the Certora team. During the verification process, the Certora Prover discovered bugs in the code 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 following section formally defines high-level specifications of the contract at hand. All the rules are publically available in a public github.