To formally verify the correctness of the Dai stablecoin ecosystem, we follow the strategy employed by Runtime Verfication to prove the correctness of the ERC20 standard using the K framework.
The process consists of the following steps;
We construct a high level, formal executable semantics of the Dai stablecoin in dai.md. The specification defines the actions and state relevant to the Dai system independent of any particular blockchain implementation. Compare with ERC20-K or the Dai purple paper.
We refine the specification to an EVM-specific semantics at dai-evm.md, outlining where and how state parameters are stored and encodes the actions according to the Ethereum contract ABI. This specification is written in eDSL and yields a suite of verifiable claims which can then be checked against a particular EVM bytecode implementation and proven correct with K's built in automated theorem prover. Compare with ERC20-EVM.