Certora Continuous Formal Verification Report April 2022
We are working on our grant proposal, stay tuned for more in the next couple of weeks.
Summary
We can’t believe it’s already been a month. In the last few weeks, we have created a beginner workshop that was held 4/27-29 with 100 registered Aave community members. We also did a verification of BGD labs streaming treasury contract.
Verification Updates
BGD labs Ecosystem Reserve v2
Described at Aave <> Bored Ghosts Developing (BGD) - #31 by EzR3aL
We have conducted a formal verification and manual audit of the ecosystem reserve contracts. It’s a modified version of Sablier money streaming protocol. The modifications allow Aave treasury to stream funds to recipients without locking them upfront, so that yield can be earned on unvested funds.
The formal verification spec includes 18 rules and invariants. These rules verify conditions like treasury solvency, correctness of withdrawal and so on.
Detailed properties description is on Github.
Certora Prover Education Updates
Certora & Aave held a beginner 3-day workshop that took place 4/27-4/29 with 100 registered Aave community members. The schedule and links to resources and recordings are below
Day 1: CVL Language - writing basic rules and understanding verification results. recording: Workshop: Aave Community Day 1 4/27/22 - YouTube
Day 2: Thinking through properties - thinking about high-level properties while working on a generic liquidity pool. Workshop: Aave Community Day 2 4/28/22 - YouTube
Day 3: Finding real bugs - practice your newly acquired skills on examples based on bugs found in the real-world.
All slides and lessons: GitHub - Certora/Tutorials: Practical tutorials of Certora Prover
Register here and get a key to the Certora Prover.
If you missed the workshop, you can still register to get a key and watch the recordings. We have Office Hours for any questions or ideas you have.
Weekly Office Hours: Wednesday, 4:30-5:30p CET
Be sure to add the calendar. We will publish more special events here.
https://bit.ly/38DDqu0 6
As we wrap up the first month of our proposal, we want to hear from you……Review our work - is there anything the community can review
-
Please give us feedback on the beginner training here (link to survey)
-
Feedback
-
Further suggestions
-
Thank the community
Thank you to this wonderful community. A special thanks to Stani and Ernesto for always answering our questions.
Email: lori@certora.com
Discord:lorib#1242
Telegram:@lblonn