Certora has formally verified Aave V4. This process covered the Liquidity Hub and Spoke contracts, along with the underlying mathematical libraries. The verification confirmed that the Solidity implementations of V4's contracts are correct according to Certora's formal rules. (Aave)