Security and Agility of Aave Smart Contracts via Continuous Formal Verification

Reading time saved: 26 minutes

18 replies, 5524 views, 54 likes


Certora's proposal 6308 to enhance Aave's smart contract security through verification and code review was passed, leading to significant contributions including the development of 16 new products and review of 51 smart contracts. Despite mixed community reactions and the end of their engagement period, Certora continues to work on Aave projects and plans to propose another year of security services.

The discussion primarily revolved around the continuation of proposal 6308, initiated by Shelly, to enhance the security of Aave's smart contracts through formal verification and manual code review, backed by Certora1. Certora, with its team of over 80 experts, has significantly contributed to Aave's security, leading to the development of 16 new products, the listing of 12 new tokens, and the review of 51 smart contracts1.

The proposal included a plan to allocate more resources, improve their Prover, develop new open-source technology, and develop a monitoring framework1. It also proposed a pricing plan of $2.7M per year, with an additional $400,000 for fellowships and community grants1. However, this was met with mixed reactions from the community, with Fig questioning the need for another grant program2, and Bgdlabs expressing strong support3.

Following community feedback, Certora decided to fund the grant program at the original sum of $400K per year, reducing the total cost of the proposal to $2.7M1. The proposal was put to a vote and passed with 651k supporting votes from 200 distinct addresses10.

Certora has since been actively working on several projects for Aave, including the release of a report on Aave's PR of fixes to the live V3 core contracts named V3.0.1, the verification report of Price sync for stable coins, and the verification report of Aave's Proof Of Reserve11. They have also been involved in the verification of the GHO token and the staticAToken which extends the ERC4626 standard14,15.

Community Security Reviews were conducted for multiple contracts, with the findings incorporated into the official reports and resulting in the distribution of $363,500 worth of grants19. Certora also conducted checks on several ERC20 tokens for potential listing in various markets19.

Despite the official end of their engagement period, MCERFSR assured the community that they are not disappearing and are currently crafting a new proposal for another year of continuous security for Aave, including community engagement19.

Posted a year ago

Last reply 3 months ago

Summary updated 2 months ago

Last updated 06/12 00:43