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 Post-Quantum Cryptography (PQC) standards represents a significant step forward in securing the Internet, and organizations across the globe, against the future threat of quantum computers.

At Cryspen, we have been developing formally verified open-source implementations of post-quantum cryptographic algorithms in Rust using the hax toolchain. Our implementations are verified to be panic free, functionally correct, and secret independent. Indeed, our verification of Kyber already uncovered vulnerabilities that were found to be present and exploitable in multiple Kyber implementations.

We have been working with Mozilla to upstream our verified implementations into the NSS cryptographic library. We are also contributing our Rust code to the PQCP project hosted by the Post Quantum Crypto Alliance.

And now, we are happy to announce that we are also partnering with Google to develop formally verified open-source implementations of the NIST standards that can be consumed not only by organizations like Google, but by anyone needing to embrace the imminent PQC transition.

Cryspen provides open source high-performance, high-assurance implementations of ML-KEM (FIPS 203) and ML-DSA (FIPS 204). They will be available as Rust crates, as well as C code packages. Other versions, including those optimized for IoT devices, can be licensed on request.

Get in touch when you are interested in using our implementations, or need support transitioning to post-quantum secure security mechanisms.