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

Battle Count: 50

The paper is primarily a formal verification contribution rather than a quantitative trading methodology. However, it has indirect relevance: (1) understanding rounding bounds informs MEV/arbitrage strategy design in DeFi; (2) the no-rounding-arbitrage property is relevant to market-making strategies on AMMs; (3) tick-crossing dynamics affect liquidity provision strategies; (4) the epsilon-slack quantification helps assess execution risk in large swaps. The paper does not propose trading signals, portfolio strategies, or predictive models.

Requires expertise in formal methods (timed automata, TLA+, temporal logic), understanding of AMM mechanics (constant-product curves, virtual reserves, tick structures), and proficiency with model-checking tools (UPPAAL, TLC). The mathematical proofs are elementary but the modeling framework is sophisticated. Implementing the full PTA network in UPPAAL or scaling TLA+ models to realistic parameter regimes presents significant state-space challenges. The TLA+ toy models are accessible but extending to production-scale verification is complex.

The paper provides concrete TLA+ module specifications (ToyCLAMM, ToyCLAMM2Dir, ToyCLAMM2DirArb, ToyCLAMM3Tick) with explicit parameter values (Bx=By=10, LMax, NMax), TLC configuration details, and state-space statistics. The mathematical proofs (Lemma 1, Theorem 1) are self-contained and elementary. However, no explicit GitHub repository URL is provided, and the full TLA+ source code is not directly linked. The PTA/UPPAAL instantiation is described but not fully implemented in the paper.