Djed: A Formally Verified Crypto-Backed Pegged Algorithmic Stablecoin

Joachim Zahnentferner; Dmytro Kaidalov; Jean-Frédéric Etienne; Javier Díaz

Paper 2021/1069

Djed: A Formally Verified Crypto-Backed Pegged Algorithmic Stablecoin

Joachim Zahnentferner

Dmytro Kaidalov

Jean-Frédéric Etienne

Javier Díaz

Abstract

This paper describes Djed, an algorithmic stablecoin protocol that behaves like an autonomous bank that buys and sells stablecoins for a price in a range that is pegged to a target price. It is crypto-backed in the sense that the bank keeps a volatile cryptocurrency in its reserve. The reserve is used to buy stablecoins from users that want to sell them. And revenue from sales of stablecoins to users are stored in the reserve. Besides stablecoins, the bank also trades reservecoins in order to capitalize itself and maintain a reserve ratio significantly greater than one. To the best of our knowledge, this is the first stablecoin protocol where stability claims are precisely and mathematically stated and proven. Furthermore, the claims and their proofs are formally verified using two different techniques: bounded model checking, to exhaustively search for counter-examples to the claims; and interactive theorem proving, to build rigorous formal proofs using a proof assistant with automated theorem proving features.

Metadata

Available format(s): PDF
Category: Applications
Publication info: Published elsewhere. Major revision. 2023 IEEE International Conference on Blockchain and Cryptocurrency (ICBC)
DOI: 10.1109/ICBC56567.2023.10174901
Keywords: Blockchain Cryptocurrency Stablecoin
Contact author(s): zahnentferner @ gmail com
dmtr kd @ gmail com
jean-frederic etienne @ iohk io
javier diaz @ iohk io
History: 2024-01-26: revised; 2021-08-23: received; See all versions
Short URL: https://ia.cr/2021/1069
License: CC BY

BibTeX

@misc{cryptoeprint:2021/1069,
      author = {Joachim Zahnentferner and Dmytro Kaidalov and Jean-Frédéric Etienne and Javier Díaz},
      title = {Djed: A Formally Verified Crypto-Backed Pegged Algorithmic Stablecoin},
      howpublished = {Cryptology ePrint Archive, Paper 2021/1069},
      year = {2021},
      doi = {10.1109/ICBC56567.2023.10174901},
      note = {\url{https://eprint.iacr.org/2021/1069}},
      url = {https://eprint.iacr.org/2021/1069}
}