This document describes the specification and verification of Aave V4 Hub using the Certora Prover. 

The detailed findings and the Aave responses can be found in the full report below.