ERC4626 Workshop

Repository alongside the Certora workshop on ERC4626 at TrustX @ Istanbul 2023.

Getting started

1. Familiarize yourself with the ERC4626 specification and take a look at the (buggy) implementation of ERC4626 under src.
2. To get to know CVL take a look at the example specification under certora/specs/Example.spec.
3. Sign-up for Certora Free Tier
4. Install the Certora prover following all steps from our official Documentation).

• Note: It's important to also set the CERTORAKEY evnrionemnt variable.

5. Run the specification by executing certoraRun certora/conf/Example.conf from within this folder. Follow the link returned and wait for the verification to be completed. Alternatively, open the pre-computed results.
6. Inspect the results and make yourself familiar with the output. Why does the rule assetAndShareMonotonicity fail for method redeem? Can you spot the mistake in the rule?
7. Think about properties of ERC4626 and note them down in https://docs.google.com/document/d/116HDhYT8pJMD9DOdrS8NdWdvTnOdsIcEQK9AjnxpdnY/edit

Write your own CVL specifications

1. Open the file certora/specs/Tutorial.spec.
2. The file contains three rule signatures that need to be implemented. Take a look at the comment and write the specifications.
3. Run Certora by executing certoraRun certora/conf/Tutorial.conf and iterate.
4. The solutions are found in branch solutions.
5. On branch solutions there is a Properties.md file that lists basic properties for ERC4626. Enhance your CVL specifications to also cover those properties. Which ones can you prove?

Additional Material

• Prover Documentation
• ERC-4626 Specifications
• Inflation Attack