Skip to content

[Certora] Add Certora verification for BabylonSpoke - #1377

Open
lilCertora wants to merge 4 commits into
aave:feat/babylon-spokefrom
Certora:feat/babylon-spoke
Open

lilCertora wants to merge 4 commits into
aave:feat/babylon-spokefrom
Certora:feat/babylon-spoke

Conversation

@lilCertora

Copy link
Copy Markdown

Adds Certora specifications, harnesses and configurations for BabylonSpoke covering:

  • Collateral restrictions: only the managed reserve can be collateral, users have at most one collateral and one debt reserve, and the managed reserve cannot be borrowed.
  • Repayment bounds: the requested payment does not exceed debtToCover or the user's debt in the selected reserve.
  • Collateral removal: the removed amount and the collateral balance reduction enforce the cap.
  • Liquidation pricing: the removed collateral value does not exceed the payment value times liquidationBonus / 10000.
  • Settlement: repayment targets the correct debt reserve, collateral removal targets the liquidator, and deficit reporting follows the remaining collateral and debt.

Adds a GitHub Actions workflow for collateral restrictions, repayment bounds, collateral removal bounds and settlement accounting.

@lilCertora lilCertora changed the title [Certora] [Certora] Add Certora verification for BabylonSpoke Oct 14, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant