This document describes the specification and verification of Aave's GHO Token using the Certora Prover. The work was undertaken from the 30th of January 2023 to the 28th of February 2023. The latest commit that was reviewed and ran through the Certora Prover was ce49fb0. The scope of our verification includes the following contracts:

GhoToken.sol

GhoDiscountRateStrategy.sol

GhoInterestRateStrategy.sol

GhoAToken.sol

GhoVariableDebtToken.sol

GhoFlashMinter.sol

GhoOracle.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 next section formally defines high level specifications of Aave's GHO Token. All the rules are publically available in a public github.