Pqc

/images/posts/cut-crystal.jpeg
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 …

/images/posts/crystals.jpeg
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 …