Cryptology ePrint Archive: Report 2021/1069

Djed: A Formally Verified Crypto-Backed Pegged Algorithmic Stablecoin

Joachim Zahnentferner and Dmytro Kaidalov and Jean-Frédéric Etienne and 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.

Category / Keywords: applications / Blockchain, Cryptocurrency, Stablecoin

Date: received 17 Aug 2021

Contact author: bruno woltzenlogel-paleo at iohk io, dmytro kaidalov at iohk io, jean-frederic etienne at iohk io, javier diaz at iohk io

Available format(s): PDF | BibTeX Citation

Version: 20210823:062949 (All versions of this report)

Short URL: ia.cr/2021/1069


[ Cryptology ePrint archive ]