Understand Volatility of Algorithmic Stablecoin: Modeling, Verification and Empirical Analysis
This work addresses volatility issues in algorithmic stablecoins, which are crucial for cryptocurrency users and developers, though it is incremental in applying formal verification and empirical methods to this domain.
The paper investigates whether algorithmic stablecoins are volatile by design and in practice, developing a modeling framework that identifies critical volatility conditions and performing empirical analysis on Basis Cash to connect theory with market observations.
An algorithmic stablecoin is a type of cryptocurrency managed by algorithms (i.e., smart contracts) to dynamically minimize the volatility of its price relative to a specific form of asset, e.g., US dollar. As algorithmic stablecoins have been growing rapidly in recent years, they become much more volatile than expected. In this paper, we took a deep dive into the core of algorithmic stablecoins and shared our answer to two fundamental research questions, i.e., Are algorithmic stablecoins volatile by design? Are they volatile in practice? Specifically, we introduced an in-depth study on three popular types of algorithmic stablecoins and developed a modeling framework to formalize their key design protocols. Through formal verification, the framework can identify critical conditions under which stablecoins might become volatile. Furthermore, we performed a systematic empirical analysis on real transaction activities of the Basis Cash stablecoin to relate theoretical possibilities to market observations. Lastly, we highlighted key design decisions for future development of algorithmic stablecoins.