Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Formalizing Automated Market Makers in the Lean 4 Theorem Prover

Daniele Pusceddu, Massimo Bartoletti

TL;DR

This work tackles the problem of formally verifying AMM economics by introducing a Lean 4 formalization of a constant-product AMM with reserves $r_0$ and $r_1$, enabling machine-checked proofs of properties like arbitrage and price-oracle alignment. The approach builds a modular Lean model of blockchain states, wallets, AMM pairs, and swap transactions around a constant-product swap rate $SX$, and defines networth and gain to capture users' economic outcomes. The key contributions include a closed-form gain formula $Gain(a,o,s,apply(sw))$, a sufficiency condition for optimal swaps ensuring the AMM's internal rate matches the price oracle, and an explicit arbitrage solution $x = \sqrt{\frac{o(\tau_1) \cdot r_0 \cdot r_1}{o(\tau_0)}} - r_0$, all formally mechanized and verified. The results provide a principled, abstract framework for reasoning about AMM economics, distinct from prior Coq/AoK efforts by focusing on economic mechanisms and reachable-state properties, with publicly available Lean code and a path toward exploring alternative designs.

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.

Formalizing Automated Market Makers in the Lean 4 Theorem Prover

TL;DR

This work tackles the problem of formally verifying AMM economics by introducing a Lean 4 formalization of a constant-product AMM with reserves and , enabling machine-checked proofs of properties like arbitrage and price-oracle alignment. The approach builds a modular Lean model of blockchain states, wallets, AMM pairs, and swap transactions around a constant-product swap rate , and defines networth and gain to capture users' economic outcomes. The key contributions include a closed-form gain formula , a sufficiency condition for optimal swaps ensuring the AMM's internal rate matches the price oracle, and an explicit arbitrage solution , all formally mechanized and verified. The results provide a principled, abstract framework for reasoning about AMM economics, distinct from prior Coq/AoK efforts by focusing on economic mechanisms and reachable-state properties, with publicly available Lean code and a path toward exploring alternative designs.

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.
Paper Structure (5 sections, 7 theorems, 11 equations, 6 tables)

This paper contains 5 sections, 7 theorems, 11 equations, 6 tables.

Table of Contents

  1. Introduction
  2. Formalization
  3. Results
  4. Related work
  5. Conclusions

Key Result

Proposition 1

Let $s' \in \Gamma$ be a reachable blockchain state. Then, for any minted token type $\left(\tau_0, \tau_1\right)$, its supply in $s'$ is strictly positive if and only if $s'$ has an AMM with token types $\tau_0$ and $\tau_1$.

Theorems & Definitions (10)

  • Proposition 1: Existence of AMMs vs. minted token supply
  • Lemma 2: Value expansion
  • Lemma 3: Gain of a swap
  • Lemma 4: Swap rate vs. exchange rate
  • Lemma 5: Unique direction for swap gain
  • Example 6
  • Theorem 7: Sufficient condition for optimal swaps
  • Example 8
  • Theorem 9: Arbitrage for constant-product AMMs
  • Example 10