LibMLKEM: a brand new, formally verified implementation of the post-quantum key exchange algorithm ML-KEM, built with the Ada & SPARK.

Why LibMLKEM?

• Rock-solid security: SPARK’s formal verification guarantees no errors, leaks, or type issues.
• Independent & transparent: a completely new take on ML-KEM, free from existing code biases.
• Pushing the boundaries: a benchmark for formal verification tools like SPARK, CBMC, and Kani.

Not production-ready yet!

LibMLKEM is for research and demonstration purposes only. It prioritizes security and verifiability over optimization. The constant time property hasn’t verified yet.