The strengths and limits of formal verification

Getting precise about the guarantees of formal verification in our open-source libraries.

I have learned that it is important to be precise when documenting the guarantees offered by formally verified code, and to resist the temptation of simplifying things too much in trying to reach a …

PSQ: Post-Quantum Shared Secrets Made Easy

We’re pleased to announce the PSQ protocol for establishing a hybrid post-quantum shared secret between two parties. Cryptographic protocols, which exclusively rely on classical public key …

Cryspen Welcomes Alex

We welcome Alex to Cryspen

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 …

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 …