An update from CTO Andy Milenius

The code for Multi-Collateral Dai is ready for release. This represents one of the most historic days in the history of our ambitious project, on par with Rune’s famous first Reddit post. All of the efforts of the Maker development community have been leading up to this moment, and all further efforts will flow from the release of this code. I have said for years that the work truly begins when Multi-Collateral Dai launches, as now the MKR holders have to earn their position as the finance backbone of the blockchain using their sound judgement and competitive entrepreneurship.

Today is not only important as a milestone for the Maker community, it also marks the first time ever a major dapp has been formally verified. As the Maker developer community we hope to continue to lead the way along the cutting edge of smart contract safety by producing educational material and encouraging all blockchain developers to get familiar with our existing proofs, which currently cover the entire CDP core engine contract. As always, you can ask questions in Maker chat if you are interested in reviewing our code and learning more about formal verification.

This release consists of four major components:

1. 1. The Source

1. 1. The Kovan Objects

1. 1. The MCD CLI

1. The Formal Verification Proofs

The Source

This includes a collection of Solidity source code files that have the following functionality:

• • The core Multi-Collateral Dai CDP engine

• • Adapter contracts for ETH and a simulated REP token to be used as collateral

• • Price feeds for both ETH and REP

• Auction contracts for buying and burning MKR; minting and selling MKR; and selling liquidated collateral

The MCD contracts and their documentation can be found here:

• • https://github.com/makerdao/dss

• https://github.com/makerdao/dss/wiki

The source code for the price feeds, their security module, and the medianizer:

• • https://github.com/makerdao/medianizer

• • https://github.com/makerdao/price-feed

• https://github.com/makerdao/osm

There is also a repository with deployment scripts for developers who want to try using Multi-Collateral Dai on their own private Ethereum instances:

• https://github.com/makerdao/dss-deploy

The Kovan Objects

This is a list of addresses that corresponds to the Kovan deployment of each module listed above. The verified source code is available on Etherscan.

Note that a faucet is available for the MKR governance token and the simulated REP token, so that developers can put the Kovan deployment to the test.

There is a faucet deployed at 0x2cb53ca7500d8d04888e0E348cB601CB9abe395D that will give you 10 MKR and 100 REP for you to play with the system. To claim your tokens use the following command:
seth send 0x2cb53ca7500d8d04888e0E348cB601CB9abe395D ‘gimme()’

This will only work once per address.

Core System Contracts

• • MCD_VAT: the CDP core engine, keeping track of DAI credit system accounting. The core engine is fully covered by formal verification proofs.
    0xcd726790550afcd77e9a7a47e86a3f9010af126b

• • MCD_PIT: the user-facing gateway contract for locking and drawing DAI for each collateral type. This contract holds and guards the collateral risk parameters.
    0xe7cf3198787c9a4daac73371a38f29aaeeced87e

• • MCD_CAT: the user-facing gateway contract for liquidating (biting) CDPs.
    0x2f34f22a00ee4b7a8f8bbc4eaee1658774c624e0

• • MCD_FLAP: the flap auction contract responsible for buying and burning MKR when the system has a surplus.
    0x8868bad8e74fca4505676d1b5b21ecc23328d132

• MCD_FLOP: the flop auction contract responsible for minting and selling MKR to cover bad debt.
  0x6191c9b0086c2ebf92300cc507009b53996fbffa

MKR governance token contract

• MCD_GOV: the MKR governance token contract.
  0x6052632c8f977edef616a31d67ce504fb474bb77

DAI stablecoin contracts

• • MCD_DAI: the DAI stablecoin contract
    0x444254706e8f1fb62a6ec26a7fa2b942ef672495

• MCD_JOIN_DAI: the DAI adapter responsible for minting and burning DAI.
  0xfcbecd1a2ac11a260f6ff9de400f815f2906a2bd

ETH collateral contracts

• • MCD_JOIN_ETH: the ETH adapter responsible for joining and exiting ETH collateral.
    0x3ccd75157dc0ec69141294eda7a3657a4db8a399

• • MCD_OSM_ETH: the oracle security module feeding the ETH.USD price into the system.
    0x9FfFE440258B79c5d6604001674A4722FfC0f7Bc

• MCD_FLIP_ETH: the ETH flip auction contract, responsible for selling off ETH collateral for DAI when a CDP is liquidated.
  0x32d496ad866d110060866b7125981c73642cc509

REP collateral contracts

• • MCD_JOIN_REP: the REP adapter responsible for joining and exiting REP collateral.
    0x5df073feb82b95af2b3c90ae458201b997512ff7

• • MCD_OSM_REP: the oracle security module feeding the REP.USD price into the system.
    0xf88bbdc1e2718f8857f30a180076ec38d53cf296

• MCD_FLIP_REP: the REP flip auction contract, responsible for selling off REP collateral for DAI when a CDP is liquidated
  0xC0851F73CC8DD5c0765E71980eC7E7Fd1EF74434

The MCD CLI

This is an interface that allows developers to interact with the deployed system from their command-line. It should be immediately useful for anyone looking to integrate with Multi-Collateral Dai from an off-chain system. Auction support will be added in a following release.

• https://github.com/makerdao/mcd-cli

The Formal Verification Proofs

This includes an executable specification in the K-framework using the formal semantics of EVM provided by KEVM, showing that the behavior of the Kovan EVM bytecode objects matches that of the formal specification. There is also documentation provided that details how K-framework, KEVM and the specifications work.

• https://github.com/dapphub/k-dss/

Some brief setup & installation instructions are provided for people who want to get started running the proofs of the bytecode’s correctness for themselves. More extensive documentation will be created soon, including some explanatory videos for people who are less familiar with formal verification.

Next Steps

This will be the first of multiple releases on the road to the production launch of Multi-Collateral Dai. Look for more functional modules and educational material in the coming weeks. An external code review with Trail of Bits will also start during the middle of October.

I’ve never been more excited about the future of the MakerDAO project, and I am happy to see that the MKR holders will soon have their tool to usher in the next phase of the blockchain revolution.