Continuous Formal Verification

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

  1. Please give us feedback on the beginner training here (link to survey)

  2. Feedback

  3. Further suggestions

  4. 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

3 Likes