We’re excited to announce that Tobias Reiher has joined Cryspen in July. Welcome, Tobias!

Throughout his career, Tobias has worked on security- and safety-critical systems where software correctness is essential. To achieve that level of correctness, he increasingly relied on formal verification. He brings a practitioner’s perspective, applying formal verification to real-world software rather than limiting it to abstract models.

A great example of this is RecordFlux, a toolset that turns declarative protocol specifications into formally verifiable SPARK implementations. Message parsers are notoriously difficult to implement correctly, yet they sit directly on the attack surface, making their correctness especially important. Tobias created the first version of RecordFlux and led its design and implementation for nearly seven years, evolving it from an early prototype into an advanced toolset supported by a dedicated team.

Rust has been an important part of that journey. He implemented the performance-critical components of RecordFlux in Rust and, more recently, worked on AdaCore’s Rust compiler for safety-critical applications.

At Cryspen, we have been bringing verification and Rust together for some time, and Tobias brings deep expertise in both. He joins our work on hax, our toolchain for proving the correctness of Rust code. His experience will help make formal verification more accessible, taking hax from a tool primarily used by verification experts to one that Rust developers can confidently adopt in their everyday work. We can’t wait to see what Tobias and Cryspen will build together.