I am a Formal Verification Wizard at Certora, where I work on proving correctness of smart constracts and developing the underlying methodology.  Previously, I worked as a Post-Doc at the University of Freiburg. My main research area includes SMT solving, Craig Interpolation and Software Model Checking. I am the creator of the SMT-solver SMTInterpol. I also worked as a freelancer for SatoshiLabs better known as the company that created the Trezor hardware wallet for cryptocurrencies.

Jochen Hoenicke

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.