Alex joins pereq

This month, we welcome Alexander Bentkamp (Alex) as the newest member of our team.

Alex joins us with a strong background in automated and interactive theorem proving, where his passion for formal proofs has driven a series of influential contributions. He completed his PhD at the Vrije Universiteit Amsterdam under the supervision of Jasmin Blanchette, Uwe Waldmann, and Wan Fokkink, developing a novel proof automation method for higher-order logic. The prover he co-developed based on this method went on to win the annual CASC competition multiple times and is now integrated into the Isabelle/HOL proof assistant.

Since his PhD, Alex has broadened his impact through the development of CvxLean, a framework for formal verification of optimization problem transformations, and the Lean game platform, which drives the popular Natural Numbers Game - a playful and accessible gateway for many newcomers to the Lean proof assistant.

Alex is joining our Tools and Proofs team, where his expertise in theorem proving will add a new dimension to our work on formally verifying security-critical software using our hax toolchain. We are particularly excited to see how Alex’s experience on proof automation will help pereq* level up our game to tackle larger and more complex industrial software applications.

A warm welcome to Alex!