mlkem-native
A portable C90 implementation of ML-KEM with machine-checked proofs over its C and its assembly.
Why this is listed
A FIPS 203 implementation offered under Apache 2.0, ISC and MIT, where the proved C and assembly is the whole of what the repository ships.
The repository describes mlkem-native as a secure, fast and portable C90 implementation of ML-KEM, and as a fork of the ML-KEM reference implementation. It states that all C code in its ML-KEM and FIPS 202 source directories is proved memory-safe and type-safe using CBMC, and that all AArch64 and x86_64 assembly is proved functionally correct, memory-safe and of secret-independent timing using HOL-Light.
It implements FIPS 203, is offered under Apache 2.0, ISC and MIT, and states that it is supported by the Post-Quantum Cryptography Alliance as part of the Linux Foundation. It also names liboqs, AWS-LC, rustls and Pavona among its users, which is a claim best checked against those projects rather than taken from here.
Sources
Checked against these sources on Sep 4, 2026. Listing is not endorsement, and nothing here is ranked or scored.