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

Julius Tranquilli, Naman Gupta

Concentrated-liquidity automated market makers (CLAMMs), as exemplified by Uniswap v3, are now a common primitive in decentralized finance frameworks. Their design combines continu…