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.