Certora Continuous Formal Verification Report for May and June 2023
Hi, Aave Friends!
Here’s a sneak peek at what we have been up to in the past couple of months.
Summary
-
Continuous Checks - We are continuously checking every code addition to all previously verified projects. In June, one of our tests in AAVE Token V3 caught a critical bug in CI. The bug allowed users to inflate their balance indefinitely and therefore get infinite proposition and voting power. The bug also allowed the malicious user to deflate other users’ proposition and voting power in the same action. Check out the CI run that caught it - LINK.
-
StaticAToken Community Contest - On May 17, we kicked off a formal verification security project in which we opened the static aToken V3 contract for community review. Dozens of independent security researchers participated, with a total of $40K awarded to 21 participants. 85 issues were submitted. The most significant issues were acknowledged by BGD, and fixes will be incorporated into the code base.
-
Governance V3 - We are working full force to verify the components of the new Aave governance mechanism. The governance system includes 2 repositories with 19 contracts and almost 4,000 lines of code. So far, we’ve reported multiple issues and are working closely with the developing entity, BGD, to fix them. As part of the governance project, we also recheck and review the associated voting tokens to ensure proper functionality and correct communication with the governance system.
-
GHO Stablecoin - Following the support of this TEMP CHECK by the community, we’ve reviewed the implementation of the Gho Steward.
-
Next Community Contest - On July 19, we will be starting another Aave community formal verification project. This time we will verify a live contract that is currently fully functioning in the ecosystem! Join our aave-community discord channel to stay up-to-date with the latest announcements regarding the project.
If you are interested in our work and would like to know more, feel free 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 accepting licensing applications. If 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 
.
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