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 Cryspen level up our game to tackle larger and more complex industrial software applications.

A warm welcome to Alex!