Cryspen @ VSTTE 2024

Karthik gave an invited talk on High Assurance Post-Quantum Cryptography at VSTTE 2024.

Verified Software: Theories, Tools, and Experiments is a conference that aims to advance the state of the art in software verification.

Cryspen @ Crypto 2024

Karthik gave an invited talk on Formal Methods for Cryptography at Crypto 2024.

Crypto is the top international conference on cryptography and is held every year (since 1981) in Santa Barbara, California. This year, Crypto invited Karthikeyan Bhargavan, our Chief Research …

Formally Verified Post-Quantum Cryptography

Cryspen provides high assurance, high performance open source implementations of post-quantum cryptography.

The US National Institute of Standards and Technology (NIST) just released the first three standards for Post-Quantum KEMs (ML-KEM) and Signatures (ML-DSA, SLH-DSA). This first official publication of …

Cryspen @ FMCP 2024

We gave a talk at the NIST workshop on Formal Methods within Certification Programs.

The US National Institute of Standards and Technology (NIST) publishes a number of important cryptographic standards (including upcoming ones for post-quantum cryptography), and runs the cryptographic …

Verifying Libcrux's ML-KEM

How we verified our Rust ML-KEM implementation in libcrux using hax and F*

In a recent blog post, we described Cryspen’s new Rust implementation of ML-KEM in Rust, and talked about how our high-assurance development methodology helped us find a new timing bug in …

Verified ML-KEM (Kyber) in Rust

We implemented ML-KEM in Rust and formally verified its correctness with hax

ML-KEM, previously known as Kyber, is the first post-quantum secure key-encapsulation mechanism (KEM) to get standardised by NIST in FIPS 203. Cryspen has built a new high assurance Rust …

Cryspen @ RWC 2023

At Real World Crypto 2023 in Tokyo, we gave a talk on the hacspec language, the hax tool, and the libcrux crypto library.