Formal State-Machine Models for Uniswap v3 Concentrated-Liquidity AMMs: Priced Timed Automata, Finite-State Transducers, and Provable Rounding Bounds

Paper: arXiv 2512.06203

Authors: Julius Tranquilli, Naman Gupta

Abstract

Concentrated-liquidity automated market makers (CLAMMs), as exemplified by Uniswap v3, are now a common primitive in decentralized finance frameworks. Their design combines continuous trading on constant-function curves with discrete tick boundaries at which liquidity positions change and rounding effects accumulate. While there is a body of economic and game-theoretic analysis of CLAMMs, there is negligible work that treats Uniswap v3 at the level of formal state machines amenable to model checking or theorem proving. In this paper we propose a formal modeling approach for Uniswap v3-style CLAMMs using (i) networks of priced timed automata (PTA), and (ii) finite-state transducers (FST) over discrete ticks. Positions are treated as stateful objects that transition only when the pool price crosses the ticks that bound their active range. We show how to encode the piecewise constant-product invariant, fee-growth variables, and tick-crossing rules in a PTA suitable for tools such as UPPAAL, and how to derive a tick-level FST abstraction for specification in TLA+. We define an explicit tick-wise invariant for a discretized, single-tick CLAMM model and prove that it is preserved up to a tight additive rounding bound under fee-free swaps. This provides a formal justification for the “$ε$-slack” used in invariance properties and shows how rounding enters as a controlled perturbation. We then instantiate these models in TLA+ and use TLC to exhaustively check the resulting invariants on structurally faithful instances, including a three-tick concentrated-liquidity configuration and a bounded no-rounding-only-arbitrage property in a bidirectional single-tick model. We discuss how these constructions lift to the tick-wise structure of Uniswap v3 via virtual reserves, and how the resulting properties can be phrased as PTA/TLA+ invariants about cross-tick behaviour and rounding safety.

Complexity vs Empirical Score

• Math Complexity: 7.5/10
• Empirical Rigor: 3.0/10
• Quadrant: Lab Rats — theoretically deep, empirically untested

Why this score: The paper presents a novel formal verification framework for Uniswap v3 using Priced Timed Automata (PTA), Finite-State Transducers (FST), and TLA+ model checking to formally bound rounding errors. While highly mathematically rigorous and formal in its state-machine specifications and proofs, it lacks real-world empirical backtesting or historical market data validation, relying instead on formal logic and model checkers.

Research Flowchart

  flowchart TD
    A[Research Goal: Formalize Uniswap v3 CLAMM<br/>Behavior, Invariants & Rounding Bounds] --> B[Formal Modeling Methodology]
    
    B -->|Model Type 1| C[Networks of Priced Timed Automata<br/>for UPPAAL]
    B -->|Model Type 2| D[Finite-State Transducers & TLA+ Specifications]
    
    E[Inputs: Piecewise Invariants, Tick Rules,<br/>Fee Variables & Virtual Reserves] --> B
    
    C & D --> F[Computational Process: Model Checking via TLC<br/>& Formal Proofs of Tick-wise Invariants]
    
    F --> G[Key Outcomes: Proof of Tight Additive Rounding Bounds<br/>& Verified Cross-Tick Invariants in TLA+]

Cited References (13)

1. Formalizing Automated Market Makers in the Lean 4 Theorem Prover (2024) — link
2. Concentrated Liquidity Analysis in Uniswap V3 (2022) — link
3. Timed Automata as a Formalism for Expressing Security: A Survey on Theory and Practice (2022) — link
4. A TLA+ Formal Proof of a Cross-Chain Swap (2022) — link
5. Strategic Liquidity Provision in Uniswap v3 (2021) — link
6. Uppaal SMC tutorial (2015) — link
7. On Time with Minimal Expected Cost! (2014) — link
8. Timed Automata: Semantics, Algorithms and Tools (2003) — link

0 of 13 cited works are in the corpus; resolved via arXiv source bundles, Semantic Scholar and OpenAlex. Corpus-wide: 2518 linked papers.