The Code is Ready

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. The Source
  2. The Kovan Objects
  3. The MCD CLI
  4. 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:

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

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

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

MKR governance token contract

DAI stablecoin contracts

ETH collateral contracts

REP collateral contracts

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.

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.

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.