Security and Agility of Aave Smart Contracts via Continuous Formal Verification

Governance
14

Thanks @yuradmt :smiley:

Certora Continuous Formal Verification Report January 2023

Hi, Aave Friends!

Here’s a peek at what we have been up to in the past month.

Summary

  • We’ve reviewed the upcoming upgrade of the safety module - stkToken. In our verification, we’ve found three issues - one high severity, one medium severity and one low severity. The development team promptly addressed the issues, and we are currently reviewing the fixed implementation. The report will be released along with the repository

  • We’ve reviewed the first phase of ​BGD’s rescue mission of tokens locked on Aave. In our review, we suggested adding some safety checks that will prevent insolvency of the contracts due to this delicate action. You can read the specification and the official report in BGD’s github repository.

  • We continue making progress on verifying the GHO token. So far, in our verification, 48 properties have been formally written. The report will be published next month.

  • We also started verifying the staticAToken which extends the ERC4626 standard. The report and results of this verification effort will be released along with the deployment of the token.

If you are interested in our work and would like to know more, you’re welcome to ask us questions in the forum :)

General Note

Do you want to write some rules and help secure contracts for Aave? We are still open to licensing applications. If you’re interested, fill out this form to apply for a key.
We encourage every community member to join us on our mission to formally verify Aave contracts. Who knows, you could even earn some money along the way. :upside_down_face:.

You can follow us on Twitter to hear about our latest grant announcements: Twitter
Join our Aave dedicated discord channel: Discord
Talk to us LIVE every Wednesday at 14:30 GMT: Zoom

2 Likes