[Resource Topic] 2021/1069: Djed: A Formally Verified Crypto-Backed Pegged Algorithmic Stablecoin

Welcome to the resource topic for 2021/1069

Title:
Djed: A Formally Verified Crypto-Backed Pegged Algorithmic Stablecoin

Authors: 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.

ePrint: https://eprint.iacr.org/2021/1069

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .