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

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