Unveiling the Mechanisms of DAI: A Logic-Based Approach to Stablecoin Analysis

TL;DR

This paper presents a formal, logic-based framework for analyzing the stability mechanisms of DAI, a MakerDAO stablecoin that combines crypto-collateralization with algorithmic controls. Implemented in Prolog and released as open-source, the framework encodes vault management, debt and surplus accounting, governance actions, and crisis mechanisms to enable precise simulation and theoretical study of stability under stressed scenarios. Key contributions include a modular, executable representation of DAI policies, the ability to run scenario analyses, and a demonstration of how governance, collateral types, and MKR-based recapitalization interact to maintain the peg. The approach provides a rigorous tool for researchers and practitioners to probe potential vulnerabilities, assess robustness, and guide design improvements in decentralized stablecoin systems.

Abstract

Stablecoins are digital assets designed to maintain a stable value, typically pegged to traditional currencies. Despite their growing prominence, many stablecoins have struggled to consistently meet stability expectations, and their underlying mechanisms often remain opaque and challenging to analyze. This paper focuses on the DAI stablecoin, which combines crypto-collateralization and algorithmic mechanisms. We propose a formal logic-based framework for representing the policies and operations of DAI, implemented in Prolog and released as open-source software. Our framework enables detailed analysis and simulation of DAI's stability mechanisms, providing a foundation for understanding its robustness and identifying potential vulnerabilities.

Figures (1)

• Figure 1: The overall picture of how the key concepts of DAI are interconnected. Red circles represent actors; colored circles are the three types of tokens (i.e., DAI, MKR, collateral); white circles are variables in the system; and rectangles denote actions or events