Skip to content

Commit 7c78fca

Browse files
sakulstraTepNikkyzia551eboadompavelvm5
authored
Aave v3.5 protocol (#133)
* refactor: align code for collateral and borrow asset + some gas optimization on the default path * feat: aligning the aaave protocol behavior with 4626 Aave has historically used half-up / bankers rounding, but the ecosystem has aligned behind 4626, so it makes sense for aave to follow suit. * fix: docs & align balance checks * fix: remove unnecessary double brackets * fix: forbid unhealthy self repay This(or a variant of this) was recommended by stermi for v3.4. While we did not include it back then, we decided to include it now. * fix: round down accrued to treasury # mixbytes 3 * fix: typo fix #mixbytes-5 * fix: round in favor of the protocol * opt: optimized assembly - mixbytes 9 * test: add test to ensure that accrued is rounded down on flashloans * fix: undermint to treasury * Update src/contracts/protocol/libraries/math/PercentageMath.sol Co-authored-by: Andrey <[email protected]> * feat: aligned vToken storage for GHO token this was recommended by stermi on 3.4 and we preferred to move it to 3.5 v3.3 GHO VToken (`GhoVariableDebtToken`) storage layout: ``` ╭-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------╮ | Name | Type | Slot | Offset | Bytes | Contract | +=======================================================================================================================================================================================================+ | lastInitializedRevision | uint256 | 0 | 0 | 32 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | initializing | bool | 1 | 0 | 1 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | ______gap | uint256[50] | 2 | 0 | 1600 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _nonces | mapping(address => uint256) | 52 | 0 | 32 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _domainSeparator | bytes32 | 53 | 0 | 32 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _borrowAllowances | mapping(address => mapping(address => uint256)) | 54 | 0 | 32 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _underlyingAsset | address | 55 | 0 | 20 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _userState | mapping(address => struct IncentivizedERC20.UserState) | 56 | 0 | 32 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _allowances | mapping(address => mapping(address => uint256)) | 57 | 0 | 32 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _totalSupply | uint256 | 58 | 0 | 32 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _name | string | 59 | 0 | 32 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _symbol | string | 60 | 0 | 32 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _decimals | uint8 | 61 | 0 | 1 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _incentivesController | contract IAaveIncentivesController | 61 | 1 | 20 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _ghoAToken | address | 62 | 0 | 20 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _discountToken | contract IERC20 | 63 | 0 | 20 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _discountRateStrategy | contract IGhoDiscountRateStrategy | 64 | 0 | 20 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | |-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------| | _ghoUserState | mapping(address => struct GhoVariableDebtToken.GhoUserState) | 65 | 0 | 32 | src/contracts/facilitators/aave/tokens/GhoVariableDebtToken.sol:GhoVariableDebtToken | ╰-------------------------+--------------------------------------------------------------+------+--------+-------+--------------------------------------------------------------------------------------╯ ``` v3.4 payload upgrade GHO vToken (`VariableDebtTokenMainnetInstanceGHO`) storage layout: ``` ╭-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------╮ | Name | Type | Slot | Offset | Bytes | Contract | +======================================================================================================================================================================================================+ | lastInitializedRevision | uint256 | 0 | 0 | 32 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | initializing | bool | 1 | 0 | 1 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | ______gap | uint256[50] | 2 | 0 | 1600 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | _nonces | mapping(address => uint256) | 52 | 0 | 32 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | _domainSeparator | bytes32 | 53 | 0 | 32 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | _borrowAllowances | mapping(address => mapping(address => uint256)) | 54 | 0 | 32 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | _underlyingAsset | address | 55 | 0 | 20 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | _userState | mapping(address => struct IncentivizedERC20.UserState) | 56 | 0 | 32 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | _allowances | mapping(address => mapping(address => uint256)) | 57 | 0 | 32 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | _totalSupply | uint256 | 58 | 0 | 32 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | _name | string | 59 | 0 | 32 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | _symbol | string | 60 | 0 | 32 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | _decimals | uint8 | 61 | 0 | 1 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | __deprecated_incentivesController | contract IAaveIncentivesController | 61 | 1 | 20 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | _deprecated_ghoAToken | address | 62 | 0 | 20 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | _deprecated_discountToken | address | 63 | 0 | 20 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | |-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------| | _deprecated_discountRateStrategy | address | 64 | 0 | 20 | src/VariableDebtTokenMainnetInstanceGHO.sol:VariableDebtTokenMainnetInstanceGHO | ╰-----------------------------------+--------------------------------------------------------+------+--------+-------+---------------------------------------------------------------------------------╯ ``` v3.5 GHO vToken (`VariableDebtToken`) storage layout: ``` ╭-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------╮ | Name | Type | Slot | Offset | Bytes | Contract | +==================================================================================================================================================================================================+ | lastInitializedRevision | uint256 | 0 | 0 | 32 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | initializing | bool | 1 | 0 | 1 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | ______gap | uint256[50] | 2 | 0 | 1600 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | _nonces | mapping(address => uint256) | 52 | 0 | 32 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | _domainSeparator | bytes32 | 53 | 0 | 32 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | _borrowAllowances | mapping(address => mapping(address => uint256)) | 54 | 0 | 32 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | _underlyingAsset | address | 55 | 0 | 20 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | _userState | mapping(address => struct IncentivizedERC20.UserState) | 56 | 0 | 32 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | _allowances | mapping(address => mapping(address => uint256)) | 57 | 0 | 32 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | _totalSupply | uint256 | 58 | 0 | 32 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | _name | string | 59 | 0 | 32 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | _symbol | string | 60 | 0 | 32 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | _decimals | uint8 | 61 | 0 | 1 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | __deprecated_incentivesController | contract IAaveIncentivesController | 61 | 1 | 20 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | __unusedGap | uint256[3] | 62 | 0 | 96 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | |-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------| | __deprecated_ghoUserState | bytes32 | 65 | 0 | 32 | src/contracts/protocol/tokenization/VariableDebtToken.sol:VariableDebtToken | ╰-----------------------------------+--------------------------------------------------------+------+--------+-------+-----------------------------------------------------------------------------╯ ``` * chore: bump revisions * feat: added instance of vToken for the GHO token This instance of the v token is intended to be used with vGHO as long as stkAAVE is not upgraded to remove the discount hook. * feat: Implemented additional roundings in debt and collateral calculations in base currency Rounding up the debt usd amount, so that liquidations can also happen on very small amounts. * fix: liquidation edge case Fixes an edge case in liquidation: When the liquidated collateral cannot cover the liquidation protocol fee, there is a chance that due to rounding the txn reverts. This pr fixes the edge case by rounding up, so on L377, the fee will be lowered accordingly, resulting a non reverting transferOnLiquidation. stermi 65 certora 12 * fix: correctly update rate on same asset liquidation - stermi 64 * opt: repayWithAToken skip hf validation if no collateral (#298) - stermi 66 * fix: improved precision in the eliminate deficit function + added return value * refactor: migrate to using scaled balances were possible The protocol switches between scaled and upscaled balance back and forth - sometimes unnecessarily. Therefore, this pr changes the pool operations to consistently work with the scaled balance where possible. --------- Co-authored-by: TepNik <[email protected]> Co-authored-by: Nikita <[email protected]> Co-authored-by: Pavel <[email protected]> Co-authored-by: Andrey <[email protected]> * fix: adjust allowance consumption Historically transferFrom etc have consumed ther users input as allowance. That has never really been accurate, as the users input might not actually be transferrable due to rounding, to account for that we improved the logic to consumer "up to the raw scaled up transfer amount". * fix: minor docs improvements liquidation protocol fee is rounded up, not down (in practice is still a bit arbitrary as it rounds multiple times, but the explicit part is now up) add totalSupply to the docs * docs: improve WadRayMath natsepc * fix: improve presision of HF calculation Certora managed to prove an occasion where the supply of 1 wei could reduce a users hf to to precision loss on avgLt calculation. While this is an extreme adge case on very small amounts, it makes sense to just not lose the precision if possible. Moving the hf check on borrow at the end, reduces code duplication and makes the operation more equivalent to e.g. withdraw. * fix: address informal mixbytes issues * perf: transfer gas optimization * style: align style of fetching balances & totalSupply * fix: calculateAvailableBorrows should perform same rounding as borrow * fix: readd descriptive error * fix: add zero division case * fix: LiquidationLogic round up the debt in base currency * fix: informal issues * fix: better allowance mechanism + informal issue fixes * chore: improve comment * docs: improve comment * docs: align docs * Added Aave v3.5 reports audit: add certora audit audit: add abdk Add MixBytes audit for Aave v3.5.0 fix: add all audits fix: don't prettier audits for PR V3.5 fix: remove duplicate certora audit * docs: added changelog into docs for v3.5 version * fix: remove duplicate audit * Update docs/3.5/Aave-v3.5-features.md Co-authored-by: Ernesto Boado <[email protected]> * fix: lint certora fv * fix: abdk report issues fix: update abdk audit fix: abdk report * fix: math helpers explicit tests (#2) * fix: add changeset --------- Co-authored-by: Nikita <[email protected]> Co-authored-by: Andrey <[email protected]> Co-authored-by: Ernesto Boado <[email protected]> Co-authored-by: TepNik <[email protected]> Co-authored-by: Pavel <[email protected]> Co-authored-by: StErMi <[email protected]>
1 parent d7a6412 commit 7c78fca

File tree

268 files changed

+15432
-1819
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

268 files changed

+15432
-1819
lines changed

‎.changeset/eighty-pianos-trade.md‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
---
2+
"@aave-dao/aave-v3-origin": minor
3+
---
4+
5+
Release of Aave v3.5

‎.github/workflows/certora-ATokenWithDelegation.yml‎

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -38,10 +38,8 @@ jobs:
3838
3939
- uses: Certora/certora-run-action@v1
4040
with:
41-
cli-version: 7.28.0
41+
cli-version: 7.31.0
4242
configurations: |-
43-
certora/atoken-with-delegation/conf/AToken.conf
44-
certora/atoken-with-delegation/conf/AToken-problematic-rules.conf --rule totalSupplyEqualsSumAllBalance additiveBurn additiveTransfer
4543
certora/atoken-with-delegation/conf/token-v3-general.conf
4644
certora/atoken-with-delegation/conf/token-v3-erc20.conf
4745
certora/atoken-with-delegation/conf/token-v3-delegate-basic.conf

‎.github/workflows/certora-basic.yml‎

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -38,12 +38,13 @@ jobs:
3838
3939
- uses: Certora/certora-run-action@v1
4040
with:
41-
cli-version: 7.28.0
41+
cli-version: 7.31.0
4242
configurations: |-
4343
certora/basic/conf/AToken.conf
44+
certora/basic/conf/VariableDebtToken.conf
4445
certora/basic/conf/ReserveConfiguration.conf
4546
certora/basic/conf/UserConfiguration.conf
46-
certora/basic/conf/VariableDebtToken.conf
47+
certora/basic/conf/NEW-pool-no-summarizations.conf
4748
certora/basic/conf/stableRemoved.conf
4849
certora/basic/conf/EModeConfiguration.conf
4950
certora/basic/conf/NEW-pool-simple-properties.conf --rule cannotDepositInInactiveReserve

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

Lines changed: 55 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,55 @@
1+
name: certora-math-calculations
2+
3+
concurrency:
4+
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
5+
cancel-in-progress: true
6+
7+
on:
8+
pull_request:
9+
branches:
10+
- main
11+
- certora
12+
push:
13+
branches:
14+
- main
15+
16+
workflow_dispatch:
17+
18+
jobs:
19+
verify:
20+
runs-on: ubuntu-latest
21+
if:
22+
github.event.pull_request.head.repo.full_name == github.repository || (github.event_name == 'push' &&
23+
github.ref == format('refs/heads/{0}', github.event.repository.default_branch))
24+
permissions:
25+
contents: read
26+
statuses: write
27+
pull-requests: write
28+
steps:
29+
- uses: actions/checkout@v4
30+
with:
31+
submodules: recursive
32+
33+
- name: Munged
34+
run: |
35+
cd certora/math-calculations
36+
touch applyHarness.patch
37+
make munged
38+
39+
- uses: Certora/certora-run-action@v1
40+
with:
41+
cli-version: 7.31.0
42+
configurations: |-
43+
certora/math-calculations/confs/rayMulDiv-CVL-check.conf
44+
certora/math-calculations/confs/gift_cannot_decrease_healthFactor.conf
45+
solc-versions: 0.8.27
46+
comment-fail-only: false
47+
solc-remove-version-prefix: "0."
48+
job-name: "Certora Prover Run"
49+
certora-key: ${{ secrets.CERTORAKEY }}
50+
install-java: true
51+
env:
52+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
53+
# Put back the following rule after ticket 8889 is closed
54+
# certora/basic/conf/NEW-pool-no-summarizations.conf ##### waiting for
55+

‎.github/workflows/certora-solvency.yml‎

Lines changed: 75 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
name: certora-solvency
2+
3+
concurrency:
4+
group: ${{ github.workflow }}-${{ github.event.pull_request.number || github.ref }}
5+
cancel-in-progress: true
6+
7+
on:
8+
pull_request:
9+
branches:
10+
- main
11+
- certora
12+
push:
13+
branches:
14+
- main
15+
16+
workflow_dispatch:
17+
18+
jobs:
19+
verify:
20+
runs-on: ubuntu-latest
21+
if:
22+
github.event.pull_request.head.repo.full_name == github.repository || (github.event_name == 'push' &&
23+
github.ref == format('refs/heads/{0}', github.event.repository.default_branch))
24+
permissions:
25+
contents: read
26+
statuses: write
27+
pull-requests: write
28+
steps:
29+
- uses: actions/checkout@v4
30+
with:
31+
submodules: recursive
32+
33+
- name: Munged
34+
run: |
35+
cd certora/solvency
36+
touch applyHarness.patch
37+
make munged
38+
39+
- uses: Certora/certora-run-action@v1
40+
with:
41+
cli-version: 7.31.0
42+
configurations: |-
43+
certora/solvency/confs/rayMulDiv-CVL-check.conf
44+
certora/solvency/confs/aToken-check.conf
45+
certora/solvency/confs/variableDebtToken-check.conf
46+
certora/solvency/confs/solvency/supply.conf
47+
certora/solvency/confs/solvency/withdraw.conf
48+
certora/solvency/confs/solvency/borrow.conf
49+
certora/solvency/confs/solvency/flashloan.conf
50+
certora/solvency/confs/solvency/repay-lemma.conf
51+
certora/solvency/confs/solvency/repay-main.conf
52+
certora/solvency/confs/solvency/repayWithATokens-lemma.conf
53+
certora/solvency/confs/solvency/repayWithATokens-main.conf --rule_sanity "none"
54+
certora/solvency/confs/solvency/liquidationCall/lemma-revertsIF_totDbt_of_DBTasset_is0.conf
55+
certora/solvency/confs/solvency/liquidationCall/lemma-DBTasset.conf
56+
certora/solvency/confs/solvency/liquidationCall/main-DBTasset.conf
57+
certora/solvency/confs/solvency/liquidationCall/main-COLasset.conf
58+
certora/solvency/confs/solvency/liquidationCall/lemma-COLasset.conf --rule_sanity "none"
59+
certora/solvency/confs/solvency/liquidationCall/main-COLasset-totSUP0.conf --rule_sanity "none"
60+
certora/solvency/confs/solvency/liquidationCall/lemma-COLasset-totSUP0.conf
61+
certora/solvency/confs/solvency/liquidationCall/burnBadDebt-assetINloop.conf
62+
certora/solvency/confs/solvency/liquidationCall/burnBadDebt-assetNOTINloop.conf
63+
certora/solvency/confs/solvency/liquidationCall/main-SAMEasset.conf
64+
certora/solvency/confs/solvency/liquidationCall/lemma-SAMEasset.conf
65+
solc-versions: 0.8.27
66+
comment-fail-only: false
67+
solc-remove-version-prefix: "0."
68+
job-name: "Certora Prover Run"
69+
certora-key: ${{ secrets.CERTORAKEY }}
70+
install-java: true
71+
env:
72+
GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
73+
# Put back the following rule after ticket 8889 is closed
74+
# certora/basic/conf/NEW-pool-no-summarizations.conf ##### waiting for
75+

‎.github/workflows/certora-stata.yml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,7 +38,7 @@ jobs:
3838
3939
- uses: Certora/certora-run-action@v1
4040
with:
41-
cli-version: 7.28.0
41+
cli-version: 7.31.0
4242
configurations: |-
4343
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
4444
certora/stata/conf/verifyERC4626.conf --rule maxMintMustntRevert maxDepositMustntRevert maxRedeemMustntRevert maxWithdrawMustntRevert totalAssetsMustntRevert

‎.prettierignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,3 +6,4 @@ report
66
_corpus
77
crytic-export
88
snapshots
9+
audits

‎LICENSE‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ Parameters
1010
Licensor: Aave DAO, represented by its governance smart contracts
1111

1212

13-
Licensed Work: Aave v3.3
13+
Licensed Work: Aave v3.5
1414
The Licensed Work is (c) 2025 Aave DAO, represented by its governance smart contracts
1515

1616
Additional Use Grant: You are permitted to use, copy, and modify the Licensed Work, subject to

‎README.md‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -106,6 +106,17 @@ In addition, Enigma Dark has adapted the Foundry-based fuzzing [invariant suite]
106106

107107
<br>
108108

109+
**-> Aave v3.5 - July 2025**
110+
111+
#### Predictable rounding
112+
113+
- [Certora](./audits/2025-07-14_Certora_AaveV3.5.pdf)
114+
- [StErMi](./audits/2025-07-17_StErMi_Aave-v3.5.md)
115+
- [Mixbytes](./audits/2025-07-18_MixBytes_AaveV3.5.pdf)
116+
- [ABDK](./audits/2025-07-17_ABDK_Aave-v3.5.pdf)
117+
118+
<br>
119+
109120
### Bug bounty
110121

111122
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.

‎audits/2025-07-14_Certora_AaveV3.5.pdf‎

718 KB
Binary file not shown.

0 commit comments

Comments
 (0)