[ARFC] Continuous Security Proposal Aave <> Certora

Part of our scope of engagement with the Aave DAO is to evaluate, coordinate with, and be the point of contact for security partners like Certora.

Given the history and performance of Certora on Aave and having worked with the team for the past years, we would like to say to the community that we firmly believe a renewal with Certora is a really good choice as a security partner.

The rationale of it is the following:

  • First of all, Certora has one of the best teams of security researchers in the space, not only in regards to their specialization (formal methods and verification techniques) but also holistically in the security of smart contracts and DeFi systems.
  • The technical contributors to the Aave DAO (us included) require quite frequent flexibility in terms of availability, and Certora has always fulfilled their obligations on the previous engagements.
  • Certora has always shown extra involvement with Aave, for example by always improving sets of properties, even when the project was considered as finished by the development team.
  • As we commented on our active Phase 2 scope, we believe Certora can be a good candidate to have a different party reviewing on-chain proposals. This is highly specialized BGD’s expertise at the moment, but we think that helping onboard a different party will give even more resilience to Aave.

To answer questions raised by the community, our collaboration with Certora will be similar to their previous engagement, with the following changes:

  • We will make an effort from our side to onboard them on on-chain governance proposal reviews.
  • We will act as coordinators of all Aave security needs of which we have visibility, trying to define a clear pipeline to optimize review time and consequently, delivery.
  • We have noticed that to have the best results, development teams contributing to Aave should be more involved in the formal verification procedures, by progressively integrating them into the development flow itself. This is something we started doing on BGD from Phase I, but we will keep improving.