DROPS

Document

DOI: 10.4230/OASIcs.FMBC.2024.5

Formalizing Automated Market Makers in the Lean 4 Theorem Prover

Authors: Daniele Pusceddu and Massimo Bartoletti

Published in: OASIcs, Volume 118, 5th International Workshop on Formal Methods for Blockchains (FMBC 2024)

Abstract

Automated Market Makers (AMMs) are an integral component of the decentralized finance (DeFi) ecosystem, as they allow users to exchange crypto-assets without the need for trusted authorities or external price oracles. Although these protocols are based on relatively simple mechanisms, e.g. to algorithmically determine the exchange rate between crypto-assets, they give rise to complex economic behaviours. This complexity is witnessed by the proliferation of models that study their structural and economic properties. Currently, most of theoretical results obtained on these models are supported by pen-and-paper proofs. This work proposes a formalization of constant-product AMMs in the Lean 4 Theorem Prover. To demonstrate the utility of our model, we provide mechanized proofs of key economic properties like arbitrage, that at the best of our knowledge have only been proved by pen-and-paper before.

Cite as

Daniele Pusceddu and Massimo Bartoletti. Formalizing Automated Market Makers in the Lean 4 Theorem Prover. In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024). Open Access Series in Informatics (OASIcs), Volume 118, pp. 5:1-5:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{pusceddu_et_al:OASIcs.FMBC.2024.5,
  author =	{Pusceddu, Daniele and Bartoletti, Massimo},
  title =	{{Formalizing Automated Market Makers in the Lean 4 Theorem Prover}},
  booktitle =	{5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
  pages =	{5:1--5:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-317-1},
  ISSN =	{2190-6807},
  year =	{2024},
  volume =	{118},
  editor =	{Bernardo, Bruno and Marmsoler, Diego},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.5},
  URN =		{urn:nbn:de:0030-drops-198702},
  doi =		{10.4230/OASIcs.FMBC.2024.5},
  annote =	{Keywords: Smart contracts, Ethereum, Verification, Blockchain}
}

Search Results

Documents authored by Pusceddu, Daniele

Formalizing Automated Market Makers in the Lean 4 Theorem Prover

Abstract

Cite as

Thanks for your feedback!

Could not send message