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.

翻译：稳定币是一种旨在保持价值稳定的数字资产，通常与传统货币挂钩。尽管其重要性日益增长，但许多稳定币难以持续满足稳定性预期，且其底层机制往往不透明且难以分析。本文聚焦于结合加密资产抵押与算法机制的DAI稳定币。我们提出了一种基于形式化逻辑的框架，用于表示DAI的策略与运行机制，该框架通过Prolog实现并已作为开源软件发布。我们的框架支持对DAI稳定性机制进行精细化分析与模拟，为理解其鲁棒性及识别潜在脆弱性奠定基础。