Overall, the MCD system's core contracts have been fully formally verified, and the verification of peripheral and helper contracts is ongoing. We are now currently working on the formal verification of the tokens that may be voted in as new collateral types, focusing on formally verifying the secondary contracts as well as the governance contracts in the system, and have incorporated formal verification into our continuous testing and release processes. In terms of our in-house efforts, we are leveraging klab, KEVM, and the K Framework for our Formal verification processes.
DSS Core - executable specification
Exhaustive reachability claims
EVM bytecode performs as we expect
Maker DSL / State Machine
High-level system model (K)
Exhaustive behaviour checking
Executable system documentation
Update - Formal Verification that has been completed thus far:
Dai token contract
Dai Savings Rate (DSR)
Emergency shutdown module (ESM)
The Oracle security module (OSM) has been largely completed.
Overall, the plan is to continue our formal verification efforts on the road to launching MCD, which includes updating past proofs based on the findings of our audits and bug findings.