Certora Continuous Formal Verification Report May 2022
Hi Aave Friends! Here’s is a peek at what we have been up to in May 2022
Summary
-
An ERC20 listing checking tool was released and used to check to be listed tokens
-
Our first community driven verification project to verify the StaticATokenLM contract started and finished.
-
Aave verification dashboard released.
-
25 additional licenses were handed to the community upon request.
Aave ERC20 Listing Checker
To assist with the token listing process on Aave platform, we designed a specification that helps inspect the suggested ERC20 for certain behaviors. When a token implementation runs against the specification using the Certora Prover, it supplies valuable information on the expected behavior of the asset in a relatively short time.
The specs contain rules to detect supply changes, pause on transfers and transfer tax, among other things. Since these can be potential token features and not bugs, the counterexamples that the Certora prover finds when running this spec should be seen, first and foremost ,as information about the tested token, not as a standard violation or a bug. The idea is that testing the token code against the spec provides knowledge and richer details to the community, so that it can make a more informed decision about the asset.
The repo with the specifications, the inspected contracts and a thorough explanation on the spec and the motive of each rule can be found here.
In our first release we’re happy to share the results obtained by the Prover on the following tokens:
The results for the runs along with their analysis can be found here.
Coming Soon: We will inspect several additional tokens, suggested by BGD, and display the results on a dedicated section in the dashboard. Stay tuned! 
.
Grant Plan
During May we’ve announced our grant plan for the community which allows community members to win rewards for their best effort of securing Aave and Aave related contracts. Tweet
First Community Driven Verification Project
Between the 15th-29th of May we launched our first verification project. The goal was verifying the StaticATokenLM.sol contract which is related to the starknet bridge.
Thank you to all the participants and congratulations on your winnings.
Aave Verification Dashboard
We’ve released a dashboard that gathers all the verification efforts done so far on Aave platform.
It features all the specifications written for different contracts and their results, including the Certora generated verification reports for each project.
For the duration of our work with Aave we will maintain the dashboard with the latest specifications and their results.
Certora Keys Distributed
During the past month we’ve handed 25 additional licenses to the community upon requests.
General Note
We are still open for license applications. If you’re interested in helping us securing Aave you can apply in this form for a key.
We encourage every community member to join us on our mission to formally verify Aave contracts and earn some money on the way 
.
You can follow us on twitter to hear about our latest announcements on the grant plan: Twitter
Join us in our discord channel dedicated to the AAVE Verification Project: Discord
And come talk to us every Wednesday on 14:30GMT: Zoom