OASIcs.FMBC.2024.5.pdf
- Filesize: 0.68 MB
- 13 pages
Document
Formalizing Automated Market Makers in the Lean 4 Theorem Prover
Authors
Massimo Bartoletti 
-
Part of:
Volume:
5th International Workshop on Formal Methods for Blockchains (FMBC 2024)
Series: Open Access Series in Informatics (OASIcs)
Conference: Workshop on Formal Methods for Blockchains (FMBC) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2024-05-21
File
Document Identifiers
Author Details
Cite AsGet BibTex
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)
https://doi.org/10.4230/OASIcs.FMBC.2024.5
https://doi.org/10.4230/OASIcs.FMBC.2024.5
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.
Subject Classification
ACM Subject Classification
- Software and its engineering → Formal methods
- Software and its engineering → Formal software verification
Keywords
- Smart contracts
- Ethereum
- Verification
- Blockchain
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Guillermo Angeris and Tarun Chitra. Improved price oracles: Constant function market makers. In ACM Conference on Advances in Financial Technologies (AFT), pages 80-91. ACM, 2020. URL: https://doi.org/10.1145/3419614.3423251.
- Guillermo Angeris, Hsien-Tang Kao, Rei Chiang, Charlie Noyes, and Tarun Chitra. An analysis of Uniswap markets. Cryptoeconomic Systems, 1(1), 2021. URL: https://doi.org/10.21428/58320208.c9738e64.
- Danil Annenkov, Jakob Botsch Nielsen, and Bas Spitters. Concert: a smart contract certification framework in Coq. In ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pages 215-228. ACM, 2020. URL: https://doi.org/10.1145/3372885.3373829.
- Balancer whitepaper, 2019. URL: https://balancer.finance/whitepaper/.
- Massimo Bartoletti, James Hsin yu Chiang, and Alberto Lluch-Lafuente. A theory of automated market makers in DeFi. Logical Methods in Computer Science, Volume 18, Issue 4, dec 2022. URL: https://doi.org/10.46298/lmcs-18(4:12)2022.
- Certora. Formal verification of Compound’s open-oracle with Uniswap anchor. https://files.safe.de.fi/safe/files/audit/pdf/CompoundUniswapAnchoredOpenOracleAug2020.pdf, 2020.
- Michael Egorov. Stableswap - efficient mechanism for stablecoin, 2019. URL: https://curve.fi/files/stableswap-paper.pdf.
- Uri Kirstein. Detecting corner cases in Compound V3 with formal specifications. https://medium.com/certora/detecting-corner-cases-in-compound-v3-with-formal-specifications-b7abf137fb15, 2022.
- Bhaskar Krishnamachari, Qi Feng, and Eugenio Grippo. Dynamic curves for decentralized autonomous cryptocurrency exchanges. In International Symposium on Foundations and Applications of Blockchain (FAB), volume 92 of OASIcs, pages 5:1-5:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/OASIcs.FAB.2021.5.
- Mooniswap whitepaper, 2020. URL: https://mooniswap.exchange/docs/MooniswapWhitePaper-v1.0.pdf.
- Eske Hoy Nielsen, Danil Annenkov, and Bas Spitters. Formalising decentralised exchanges in Coq. In ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pages 290-302. ACM, 2023. URL: https://doi.org/10.1145/3573105.3575685.
- Improving frontrunning resistance of x*y=k market makers, 2018. URL: https://ethresear.ch/t/improving-front-running-resistance-of-x-y-k-market-makers/1281.
- Jiahua Xu, Krzysztof Paruch, Simon Cousaert, and Yebo Feng. Sok: Decentralized exchanges (DEX) with automated market maker (AMM) protocols. ACM Comput. Surv., 55(11):238:1-238:50, 2023. URL: https://doi.org/10.1145/3570639.