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

TL;DR

This paper introduces formal models for Uniswap v3's concentrated-liquidity AMMs using timed automata and finite-state transducers, enabling rigorous verification of invariants and rounding bounds.

Contribution

It develops a formal modeling framework for Uniswap v3 CLAMMs with timed automata and transducers, and proves invariants under rounding effects.

Findings

Formal encoding of Uniswap v3 invariants in PTA and TLA+

Proof of invariant preservation up to tight rounding bounds

Exhaustive model checking confirms correctness in specific configurations

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 "$\epsilon$-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.