Formally Specifying and Testing the Rust Standard Library

Cryspen found and fixed bugs in the Rust SIMD libraries using formal specs

Modern programming languages typically come with a large standard library that implements essential language features like machine arithmetic and I/O, offers efficient data structures, provides …

Helping Secure Signal's Post-Quantum Transition

Cryspen worked with Signal to formally analyze their new post-quantum ratchet

Signal just announced the deployment of their new post-quantum ratcheting protocol, called the Sparse Post-Quantum Ratchet (SPQR), and Cryspen is proud to have contributed to the formal analysis of …

PQC Support for JZLint

MTG and Cryspen release JZLint 2.0: A tool for analyzing post-quantum certificates

We joined forces with MTG AG, a leader in public key infrastructures, to release JZLint 2.0 with support for analyzing post-quantum (PQC) certificates and their public keys.

Tooling for Automated Benchmarking and Visualization

Maintaining peak software performance is a critical aspect of our development process, and early regression detection is non-negotiable. At Cryspen, we’ve addressed this by implementing an …

Cryspen Welcomes Clement

A Warm Welcome to Clement, Our Newest Cryspen Crew Member!

The team here at Cryspen is thrilled to welcome to our newest member, Clement! Clement joins us fresh from his impressive journey as a PhD student at Inria Paris, where he was part of the Cambium …

MLS Group State Forks: What, Why, How

What are state forks, why can’t they happen but do anyway and how can they be resolved in OpenMLS?

Group state forks are faulty states that MLS groups can end up in. This article looks at what they are exactly, how that happens and how to resolve them. We also look at a new OpenMLS feature that …

Cryspen @ RWC 2025

Real World Crypto 2025 buzzed with energy as the cutting edge of cryptography was presented to and discussed among an audience of leading researchers and developers from academia and industry. Today, …

Control flow analysis with hax

A difficulty of formal verification is that specifying programs can be hard. Certain kinds of programs can end up having a specification that is as complex as the code itself. In this case it is …

Cryspen Welcomes Clara

A Warm Welcome to Clara, Our Newest Cryspen Crew Member!

We’re thrilled to officially welcome Clara to the Cryspen team! Clara brings a fantastic blend of experiences and a passion for open-source that aligns perfectly with our mission. Let’s …