fund-eq-of-dai-certora

Succinctly prove the fundamental equation of DAI fails to hold using the Certora prover.

Instructions (TODO: can be improved)

Create a Python virtual environment, activate it, install Certora CLI (make sure the CERTORAKEY env var is set to a valid key), install solc-select, use solc-select to install solc 0.8.13, clone this repo into it, run via make certora-vat.