Skip to content

Fix 404 github links, remove section for assertion that doesn't exist[GTM-2304] #175

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
czepluch merged 1 commit into from
Dec 16, 2025
Merged

Fix 404 github links, remove section for assertion that doesn't exist[GTM-2304] #175

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
19 changes: 6 additions & 13 deletions assertions-book/assertions/aave-v3-suite.mdx
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,11 +31,9 @@ In order to showcase the real power of assertions, we have introduced a bug in t

Anyone borrowing exactly `333e6` tokens will receive double the amount of tokens they would normally receive if they borrowed any other amount.

The bug can be found in the [BorrowLogic.sol](https://github.com/phylaxsystems/aave-v3-origin/tree/main/src/protocol/libraries/logic/BorrowLogic.sol#L128-L144) file.
The bug can be found in the [BorrowLogic.sol](https://github.com/phylaxsystems/aave-v3-origin/blob/main/src/contracts/protocol/libraries/logic/BorrowLogic.sol#L137-L141) file.

<Warning>
**DO NOT USE THIS VERSION OF AAVE V3 IN PRODUCTION!**
</Warning>
<Warning>**DO NOT USE THIS VERSION OF AAVE V3 IN PRODUCTION!**</Warning>

## Key Features

Expand Down Expand Up @@ -66,7 +64,7 @@ These demonstrate assertion capabilities but could be implemented in Solidity:

## Assertion Collections

### Production Assertions (High Value)
### Production Assertions

#### Core Invariants

Expand Down Expand Up @@ -97,18 +95,12 @@ These demonstrate assertion capabilities but could be implemented in Solidity:
- Balance change verification using event logs
- Works with complex call patterns

### Showcase Assertions (Demonstrative)
### Showcase Assertions

#### Operation Validation

- **[BorrowingInvariantAssertions](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/src/showcase/BorrowingInvariantAssertions.a.sol)** - Standard borrow checks:
- Liability decrease verification
- Health factor maintenance
- Reserve state consistency
- Borrow cap enforcement
- Balance/debt tracking

- **[LendingInvariantAssertions](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/src/showcase/LendingInvariantAssertions.a.sol)** - Standard supply/withdrawal checks:

- Reserve state validation
- Supply cap enforcement
- Balance change verification
Expand Down Expand Up @@ -152,6 +144,7 @@ These demonstrate assertion capabilities but could be implemented in Solidity:
## Intentional Bugs

1. **333e6 Borrow Bug**: Borrowing exactly 333e6 tokens returns double amount

- Location: `BorrowLogic.sol` lines 128-144
- Test: `test_BASE_INVARIANT_A_DebtTokenSupply_333e6Bug()`

Expand Down