Continuous Formal Verification

Following approval of the governance proposal, we are excited to be part of the Aave family. We have closely worked with the Aave dev team since V2, and we are glad to work with the community and the BGD initiative.

Personnel
The following are more concrete details about our joint work going forward:

Itay Grandenwits @itayGradenwits is a security researcher who worked on Aave V3. He is available to help you in reviewing the code changes introduced in new proposals.

Yura Sherman @yuradmt, a security engineer, is available to verify additional properties about the protocol.

Together with Nurit Dor, Itay and Yura, we will review proposed changes to the Solidity code.

In addition, our team will hold office hours every Wednesday at 3:30 pm European time via a zoom link.

Continued Verification
The verification report for Aave V3 is available at https://www.certora.com/wp-content/uploads/2022/02/AaveV3Jan2022-1.pdf. Going forward, we plan to verify more rules. If you would like to suggest more rules this will be greatly appreciated.

Certora Prover Education
We plan to deep dive into Aave V3 core implementation and teach formal verification.

A beginner workshop is scheduled to start on the week of April 25, 2022, on Monday, Tuesday, Wednesday, and Thursday 3 pm-4:30 pm European time. This workshop will provide instructions on the general use of our tool and explanations of Aave V3 implementation and properties. A second workshop, planned for May, will cover advanced topics and additional rules which were verified in V3. A third workshop, planned for summer, will cover new rules written by the community which will be reviewed by both the Aave community and the Certora team, and appropriately rewarded in Aave tokens.

Grants
As part of the proposal, a sum of up to $200K will be distributed to allow contributions from the Aave community for formal verification using the Certora Prover. Grant proposals can be submitted by posting in the forum where the Aave and Certora teams will review them and allocate following it.

Access to Certora Prover and Workshops
If you would like to have keys to access the tool and/or participant in the workshop please email lori@certora.com.

New Products and Early Availability
We are developing a new dashboard for code security. We will share the dashboard proposal in an upcoming office hours meeting

Our new path coverage tool for rules is scheduled to be available during Q2, 2022. We will start by running the fuzzer on the hardest rules from the Aave Protocol V3 verification project and present the findings to the community, following which we will allow the community to utilize the path coverage tool as part of their workflows and build systems freely.

4 Likes