Liquidity providers in an AMM expect that they can always withdraw their tokens, even in case of a bank run. Taking the concrete implementation of Uniswap v4, we formally proved that the funds owned by the contract always cover the provided liquidity. This talk describes the methodology for proving this critical property, which can be applied to other protocols holding the liquidity for their users.