V3.4.0

.github/workflows/certora-ATokenWithDelegation.yml

@@ -0,0 +1,62 @@
+name: certora-ATokenWithDelegation
+
+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/atoken-with-delegation
+          touch applyHarness.patch
+          make munged
+
+      - uses: Certora/certora-run-action@v1
+        with:
+          cli-version: 7.28.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 
+            certora/atoken-with-delegation/conf/token-v3-delegate-invariants.conf --rule mirror_votingDelegatee_correct mirror_propositionDelegatee_correct mirror_delegationMode_correct mirror_balance_correct --rule_sanity "none" 
+            certora/atoken-with-delegation/conf/token-v3-delegate-invariants.conf --exclude_rule mirror_votingDelegatee_correct mirror_propositionDelegatee_correct mirror_delegationMode_correct mirror_balance_correct 
+            certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule vp_change_in_balance_affect_power_DELEGATEE 
+            certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule vp_change_of_balance_affect_power_NON_DELEGATEE 
+            certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule pp_change_in_balance_affect_power_DELEGATEE 
+            certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule pp_change_of_balance_affect_power_NON_DELEGATEE 
+            certora/atoken-with-delegation/conf/token-v3-delegate-HL-rules.conf --rule no_function_changes_both_balance_and_delegation_state
+          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 }}

.github/workflows/certora-basic.yml

@@ -7,8 +7,8 @@ concurrency:
 on:
   pull_request:
     branches:
-      - certora
       - main
+      - certora
   push:
     branches:
       - main
@@ -21,56 +21,48 @@ jobs:
     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: Install python
-        uses: actions/setup-python@v5
-        with: { python-version: 3.9 }
-
-      - name: Install java
-        uses: actions/setup-java@v4
-        with: { distribution: "zulu", java-version: "11", java-package: jre }
-
-      - name: Install certora cli
-        run: pip install certora-cli==7.20.3
-
-      - name: Install solc
-        run: |
-          wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux
-          chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc8.19
-
-      - name: Verify rule ${{ matrix.rule }}
+      - name: Munged
         run: |
           cd certora/basic
           touch applyHarness.patch
           make munged
-          cd ../..
-          echo "key length" ${#CERTORAKEY}
-          certoraRun certora/basic/conf/${{ matrix.rule }} --wait_for_results
+
+      - uses: Certora/certora-run-action@v1
+        with:
+          cli-version: 7.28.0
+          configurations: |-
+            certora/basic/conf/AToken.conf
+            certora/basic/conf/ReserveConfiguration.conf
+            certora/basic/conf/UserConfiguration.conf
+            certora/basic/conf/VariableDebtToken.conf
+            certora/basic/conf/stableRemoved.conf
+            certora/basic/conf/EModeConfiguration.conf
+            certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotDepositInInactiveReserve
+            certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotDepositInFrozenReserve
+            certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotDepositZeroAmount
+            certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotWithdrawZeroAmount
+            certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotWithdrawFromInactiveReserve
+            certora/basic/conf/NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowZeroAmount
+            certora/basic/conf/NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnInactiveReserve
+            certora/basic/conf/NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnReserveDisabledForBorrowing
+            certora/basic/conf/NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnFrozenReserve
+          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:
-          CERTORAKEY: ${{ secrets.CERTORAKEY }}
+          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
 
-    strategy:
-      fail-fast: false
-      max-parallel: 16
-      matrix:
-        rule:
-          - AToken.conf
-          - ReserveConfiguration.conf
-          - UserConfiguration.conf
-          - VariableDebtToken.conf
-          - NEW-pool-no-summarizations.conf
-          - stableRemoved.conf
-          - EModeConfiguration.conf
-          - NEW-pool-simple-properties.conf --rule cannotDepositInInactiveReserve --msg "cannotDepositInInactiveReserve"
-          - NEW-pool-simple-properties.conf --rule cannotDepositInFrozenReserve --msg "cannotDepositInFrozenReserve"
-          - NEW-pool-simple-properties.conf --rule cannotDepositZeroAmount --msg "cannotDepositZeroAmount"
-          - NEW-pool-simple-properties.conf --rule cannotWithdrawZeroAmount --msg "cannotWithdrawZeroAmount"
-          - NEW-pool-simple-properties.conf --rule cannotWithdrawFromInactiveReserve --msg "cannotWithdrawFromInactiveReserve"
-          - NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowZeroAmount --msg "cannotBorrowZeroAmount"
-          - NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnInactiveReserve --msg "cannotBorrowOnInactiveReserve"
-          - NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnReserveDisabledForBorrowing --msg "cannotBorrowOnReserveDisabledForBorrowing"
-          - NEW-pool-simple-properties.conf --rule_sanity none --rule cannotBorrowOnFrozenReserve --msg "cannotBorrowOnFrozenReserve"

.github/workflows/certora-stata.yml

@@ -1,10 +1,15 @@
 name: certora-stata
 
+concurrency:
+  group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
 on:
-  push:
+  pull_request:
     branches:
       - main
-  pull_request:
+      - certora
+  push:
     branches:
       - main
 
@@ -16,65 +21,53 @@ jobs:
     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: Install python
-        uses: actions/setup-python@v5
-        with: { python-version: 3.9 }
-
-      - name: Install java
-        uses: actions/setup-java@v4
-        with: { distribution: "zulu", java-version: "11", java-package: jre }
-
-      - name: Install certora cli
-        run: pip install certora-cli==7.20.3
-      - name: Install solc
-        run: |
-          wget https://github.com/ethereum/solidity/releases/download/v0.8.20/solc-static-linux
-          chmod +x solc-static-linux
-          sudo mv solc-static-linux /usr/local/bin/solc8.20
-
-      - name: Verify rule ${{ matrix.rule }}
+      - name: Munged
         run: |
           cd certora/stata
           touch applyHarness.patch
           make munged
-          cd ../..
-          certoraRun certora/stata/conf/${{ matrix.rule }}
-        env:
-          CERTORAKEY: ${{ secrets.CERTORAKEY }}
 
-    strategy:
-      fail-fast: false
-      max-parallel: 16
-      matrix:
-        rule:
-          - 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
-          - verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert
-          # Timeout
-          # - verifyERC4626.conf --rule previewWithdrawIndependentOfMaxWithdraw
-          - verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay
-          - verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1
-          - verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint maxDepositConstant
-          - verifyERC4626Extended.conf --rule redeemSum
-          - verifyERC4626Extended.conf --rule redeemATokensSum
-          - verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf
-          - verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf
-          - verifyStataToken.conf --rule rewardsConsistencyWhenSufficientRewardsExist
-          - verifyStataToken.conf --rule rewardsConsistencyWhenInsufficientRewards
-          - verifyStataToken.conf --rule totalClaimableRewards_stable
-          - verifyStataToken.conf --rule solvency_positive_total_supply_only_if_positive_asset
-          - verifyStataToken.conf --rule solvency_total_asset_geq_total_supply
-          - verifyStataToken.conf --rule singleAssetAccruedRewards
-          - verifyStataToken.conf --rule totalAssets_stable
-          - verifyStataToken.conf --rule getClaimableRewards_stable
-          - verifyStataToken.conf --rule getClaimableRewards_stable_after_deposit
-          - verifyStataToken.conf --rule getClaimableRewards_stable_after_refreshRewardTokens
-          - verifyStataToken.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf
-          - verifyStataToken.conf --rule rewardsTotalDeclinesOnlyByClaim
-          - verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_sufficient
-          - verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient
+      - uses: Certora/certora-run-action@v1
+        with:
+          cli-version: 7.28.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
+            certora/stata/conf/verifyERC4626MintDepositSummarization.conf --rule depositCheckIndexGRayAssert2 depositATokensCheckIndexGRayAssert2 depositWithPermitCheckIndexGRayAssert2 depositCheckIndexERayAssert2 depositATokensCheckIndexERayAssert2 depositWithPermitCheckIndexERayAssert2 mintCheckIndexGRayUpperBound mintCheckIndexGRayLowerBound mintCheckIndexEqualsRay
+            certora/stata/conf/verifyERC4626DepositSummarization.conf --rule depositCheckIndexGRayAssert1 depositATokensCheckIndexGRayAssert1 depositWithPermitCheckIndexGRayAssert1 depositCheckIndexERayAssert1 depositATokensCheckIndexERayAssert1 depositWithPermitCheckIndexERayAssert1
+            certora/stata/conf/verifyERC4626Extended.conf --rule previewWithdrawRoundingRange previewRedeemRoundingRange amountConversionPreserved sharesConversionPreserved accountsJoiningSplittingIsLimited convertSumOfAssetsPreserved previewDepositSameAsDeposit previewMintSameAsMint maxDepositConstant
+            certora/stata/conf/verifyERC4626Extended.conf --rule redeemSum
+            certora/stata/conf/verifyERC4626Extended.conf --rule redeemATokensSum
+            certora/stata/conf/verifyAToken.conf --rule aTokenBalanceIsFixed_for_collectAndUpdateRewards aTokenBalanceIsFixed_for_claimRewards aTokenBalanceIsFixed_for_claimRewardsOnBehalf
+            certora/stata/conf/verifyAToken.conf --rule aTokenBalanceIsFixed_for_claimSingleRewardOnBehalf aTokenBalanceIsFixed_for_claimRewardsToSelf
+            certora/stata/conf/verifyStataToken.conf --rule rewardsConsistencyWhenSufficientRewardsExist
+            certora/stata/conf/verifyStataToken.conf --rule rewardsConsistencyWhenInsufficientRewards
+            certora/stata/conf/verifyStataToken.conf --rule totalClaimableRewards_stable
+            certora/stata/conf/verifyStataToken.conf --rule solvency_positive_total_supply_only_if_positive_asset
+            certora/stata/conf/verifyStataToken.conf --rule solvency_total_asset_geq_total_supply
+            certora/stata/conf/verifyStataToken.conf --rule singleAssetAccruedRewards
+            certora/stata/conf/verifyStataToken.conf --rule totalAssets_stable
+            certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable
+            certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable_after_deposit
+            certora/stata/conf/verifyStataToken.conf --rule getClaimableRewards_stable_after_refreshRewardTokens
+            certora/stata/conf/verifyStataToken.conf --rule getClaimableRewardsBefore_leq_claimed_claimRewardsOnBehalf
+            certora/stata/conf/verifyStataToken.conf --rule rewardsTotalDeclinesOnlyByClaim
+            certora/stata/conf/verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_sufficient
+            certora/stata/conf/verifyDoubleClaim.conf --rule prevent_duplicate_reward_claiming_single_reward_insufficient
+          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 }}

.gitignore

@@ -1,6 +1,7 @@
 # build and cache
 cache/
 out/
+zkout/
 
 # general
 .env
@@ -36,4 +37,5 @@ resource_errors.json
 
 # invariants
 _corpus/
-crytic-export/
+crytic-export/
+slither_results.json

Makefile

@@ -43,15 +43,13 @@ git-diff :
 
 # Deploy
 deploy-libs-one	:;
-	FOUNDRY_PROFILE=${chain} forge script scripts/misc/LibraryPreCompileOne.sol --rpc-url ${chain} --ledger --mnemonic-indexes ${MNEMONIC_INDEX} --sender ${LEDGER_SENDER} --slow --broadcast
+	FOUNDRY_PROFILE=${chain} forge script scripts/misc/LibraryPreCompileOne.sol --rpc-url ${chain} --ledger --mnemonic-indexes ${MNEMONIC_INDEX} --sender ${LEDGER_SENDER} --slow --broadcast --verify
 deploy-libs-two	:;
-	FOUNDRY_PROFILE=${chain} forge script scripts/misc/LibraryPreCompileTwo.sol --rpc-url ${chain} --ledger --mnemonic-indexes ${MNEMONIC_INDEX} --sender ${LEDGER_SENDER} --slow --broadcast
+	FOUNDRY_PROFILE=${chain} forge script scripts/misc/LibraryPreCompileTwo.sol --rpc-url ${chain} --ledger --mnemonic-indexes ${MNEMONIC_INDEX} --sender ${LEDGER_SENDER} --slow --broadcast --verify
 
 deploy-libs :
 	make deploy-libs-one chain=${chain}
-	npx catapulta-verify -b broadcast/LibraryPreCompileOne.sol/${chainId}/run-latest.json
 	make deploy-libs-two chain=${chain}
-	npx catapulta-verify -b broadcast/LibraryPreCompileTwo.sol/${chainId}/run-latest.json
 
 
 # Invariants

README.md

@@ -95,6 +95,17 @@ In addition, Enigma Dark has adapted the Foundry-based fuzzing [invariant suite]
 
 <br>
 
+**-> Aave v3.4 - June 2025**
+
+#### Removal of custom GHO. Addition of Multicall & Position manager
+
+- [Certora v3.4](./audits/2025-06-11_Certora_Aave-v3.4_Report.pdf), [Certora v3.4 AIP](./audits/2025-06-11_Certora_Aave-v3.4_AIP_Report.pdf)
+- [StErMi v3.4](./audits/2025-06-11_Stermi_Aave-v3.4_Report.pdf), [StErMi v3.4 AIP](./audits/2025-06-11_Stermi_Aave-v3.4_AIP_Report.pdf)
+- [Blackthorn](./audits/2025-06-12_Blackthorn-v3.4_Report.pdf)
+- [Enigma](./audits/2025-05-13_Enigma_Aave-v3.4.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.