Aave v3.5 protocol

.changeset/eighty-pianos-trade.md

@@ -0,0 +1,5 @@
+---
+"@aave-dao/aave-v3-origin": minor
+---
+
+Release of Aave v3.5

.github/workflows/certora-ATokenWithDelegation.yml

@@ -38,10 +38,8 @@ jobs:
 
       - uses: Certora/certora-run-action@v1
         with:
-          cli-version: 7.28.0
+          cli-version: 7.31.0
           configurations: |-
-            certora/atoken-with-delegation/conf/AToken.conf 
-            certora/atoken-with-delegation/conf/AToken-problematic-rules.conf --rule totalSupplyEqualsSumAllBalance additiveBurn additiveTransfer 
             certora/atoken-with-delegation/conf/token-v3-general.conf 
             certora/atoken-with-delegation/conf/token-v3-erc20.conf 
             certora/atoken-with-delegation/conf/token-v3-delegate-basic.conf 

.github/workflows/certora-basic.yml

@@ -38,12 +38,13 @@ jobs:
 
       - uses: Certora/certora-run-action@v1
         with:
-          cli-version: 7.28.0
+          cli-version: 7.31.0
           configurations: |-
             certora/basic/conf/AToken.conf
+            certora/basic/conf/VariableDebtToken.conf
             certora/basic/conf/ReserveConfiguration.conf
             certora/basic/conf/UserConfiguration.conf
-            certora/basic/conf/VariableDebtToken.conf
+            certora/basic/conf/NEW-pool-no-summarizations.conf
             certora/basic/conf/stableRemoved.conf
             certora/basic/conf/EModeConfiguration.conf
             certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotDepositInInactiveReserve

.github/workflows/certora-math-calculations.yml

@@ -0,0 +1,55 @@
+name: certora-math-calculations
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+on:
+  pull_request:
+    branches:
+      - main
+      - certora
+  push:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    if:
+      github.event.pull_request.head.repo.full_name == github.repository || (github.event_name == 'push' &&
+      github.ref == format('refs/heads/{0}', github.event.repository.default_branch))
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Munged
+        run: |
+          cd certora/math-calculations
+          touch applyHarness.patch
+          make munged
+
+      - uses: Certora/certora-run-action@v1
+        with:
+          cli-version: 7.31.0
+          configurations: |-
+            certora/math-calculations/confs/rayMulDiv-CVL-check.conf
+            certora/math-calculations/confs/gift_cannot_decrease_healthFactor.conf
+          solc-versions: 0.8.27
+          comment-fail-only: false
+          solc-remove-version-prefix: "0."
+          job-name: "Certora Prover Run"
+          certora-key: ${{ secrets.CERTORAKEY }}
+          install-java: true
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+# Put back the following rule after ticket 8889 is closed
+# certora/basic/conf/NEW-pool-no-summarizations.conf ##### waiting for
+

.github/workflows/certora-solvency.yml

@@ -0,0 +1,75 @@
+name: certora-solvency
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+on:
+  pull_request:
+    branches:
+      - main
+      - certora
+  push:
+    branches:
+      - main
+
+  workflow_dispatch:
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    if:
+      github.event.pull_request.head.repo.full_name == github.repository || (github.event_name == 'push' &&
+      github.ref == format('refs/heads/{0}', github.event.repository.default_branch))
+    permissions:
+      contents: read
+      statuses: write
+      pull-requests: write
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
+      - name: Munged
+        run: |
+          cd certora/solvency
+          touch applyHarness.patch
+          make munged
+
+      - uses: Certora/certora-run-action@v1
+        with:
+          cli-version: 7.31.0
+          configurations: |-
+            certora/solvency/confs/rayMulDiv-CVL-check.conf 
+            certora/solvency/confs/aToken-check.conf 
+            certora/solvency/confs/variableDebtToken-check.conf 
+            certora/solvency/confs/solvency/supply.conf 
+            certora/solvency/confs/solvency/withdraw.conf 
+            certora/solvency/confs/solvency/borrow.conf 
+            certora/solvency/confs/solvency/flashloan.conf 
+            certora/solvency/confs/solvency/repay-lemma.conf 
+            certora/solvency/confs/solvency/repay-main.conf 
+            certora/solvency/confs/solvency/repayWithATokens-lemma.conf 
+            certora/solvency/confs/solvency/repayWithATokens-main.conf --rule_sanity "none" 
+            certora/solvency/confs/solvency/liquidationCall/lemma-revertsIF_totDbt_of_DBTasset_is0.conf 
+            certora/solvency/confs/solvency/liquidationCall/lemma-DBTasset.conf 
+            certora/solvency/confs/solvency/liquidationCall/main-DBTasset.conf 
+            certora/solvency/confs/solvency/liquidationCall/main-COLasset.conf 
+            certora/solvency/confs/solvency/liquidationCall/lemma-COLasset.conf --rule_sanity "none" 
+            certora/solvency/confs/solvency/liquidationCall/main-COLasset-totSUP0.conf --rule_sanity "none" 
+            certora/solvency/confs/solvency/liquidationCall/lemma-COLasset-totSUP0.conf 
+            certora/solvency/confs/solvency/liquidationCall/burnBadDebt-assetINloop.conf 
+            certora/solvency/confs/solvency/liquidationCall/burnBadDebt-assetNOTINloop.conf 
+            certora/solvency/confs/solvency/liquidationCall/main-SAMEasset.conf 
+            certora/solvency/confs/solvency/liquidationCall/lemma-SAMEasset.conf
+          solc-versions: 0.8.27
+          comment-fail-only: false
+          solc-remove-version-prefix: "0."
+          job-name: "Certora Prover Run"
+          certora-key: ${{ secrets.CERTORAKEY }}
+          install-java: true
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+# Put back the following rule after ticket 8889 is closed
+# certora/basic/conf/NEW-pool-no-summarizations.conf ##### waiting for
+

.github/workflows/certora-stata.yml

@@ -38,7 +38,7 @@ jobs:
 
       - uses: Certora/certora-run-action@v1
         with:
-          cli-version: 7.28.0
+          cli-version: 7.31.0
           configurations: |-
             certora/stata/conf/verifyERC4626.conf --rule previewRedeemIndependentOfBalance previewMintAmountCheck previewDepositIndependentOfAllowanceApprove previewWithdrawAmountCheck previewWithdrawIndependentOfBalance2 previewWithdrawIndependentOfBalance1 previewRedeemIndependentOfMaxRedeem1 previewRedeemAmountCheck previewRedeemIndependentOfMaxRedeem2 amountConversionRoundedDown withdrawCheck redeemCheck redeemATokensCheck convertToAssetsCheck convertToSharesCheck toAssetsDoesNotRevert sharesConversionRoundedDown toSharesDoesNotRevert previewDepositAmountCheck maxRedeemCompliance maxWithdrawConversionCompliance previewMintIndependentOfAllowance
             certora/stata/conf/verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert

.prettierignore

@@ -6,3 +6,4 @@ report
 _corpus
 crytic-export
 snapshots
+audits

LICENSE

@@ -10,7 +10,7 @@ Parameters
 Licensor:             Aave DAO, represented by its governance smart contracts
 
 
-Licensed Work:        Aave v3.3
+Licensed Work:        Aave v3.5
                       The Licensed Work is (c) 2025 Aave DAO, represented by its governance smart contracts
 
 Additional Use Grant: You are permitted to use, copy, and modify the Licensed Work, subject to

README.md

@@ -106,6 +106,17 @@ In addition, Enigma Dark has adapted the Foundry-based fuzzing [invariant suite]
 
 <br>
 
+**-> Aave v3.5 - July 2025**
+
+#### Predictable rounding
+
+- [Certora](./audits/2025-07-14_Certora_AaveV3.5.pdf)
+- [StErMi](./audits/2025-07-17_StErMi_Aave-v3.5.md)
+- [Mixbytes](./audits/2025-07-18_MixBytes_AaveV3.5.pdf)
+- [ABDK](./audits/2025-07-17_ABDK_Aave-v3.5.pdf)
+
+<br>
+
 ### Bug bounty
 
 This repository will be subjected to [this bug bounty](https://immunefi.com/bounty/aave/) once the Aave Governance upgrades the smart contracts in the applicable production instances.