source

ml_kem

1.0.0

SPARK-proved ML-KEM (FIPS 203) lattice-based key encapsulation

GitHub Community CIResults Version page Download JSON

1.0.0

SPARK-proved ML-KEM (Module-Lattice-Based Key-Encapsulation Mechanism) implementing NIST FIPS 203. Formally verified at SPARK level 2 with zero pragma Assume, zero unproved VCs. The 7-layer Cooley-Tukey NTT, BaseMul, IndCPA, and FO transform are all proved end-to-end with no escape hatches.

All three FIPS 203 parameter sets -- ML-KEM-512, ML-KEM-768, ML-KEM-1024 -- are supported and selected at build time via the parameter_set crate configuration variable; default is ML-KEM-768 (NIST Category III).

Proof techniques are documented in PROOF_NOTES.md and reusable for similar lattice / ARX cryptography.

Built on sha3_ada for SHA-3/SHAKE. No heap allocation, pragma Pure, suitable for embedded and safety-critical systems. Constant-time execution empirically verified via cachegrind (LLd byte-identical). FIPS 140-3 validation is out of scope. See SECURITY.md for the full threat model.

Authors
Baris Erdem
Maintainers
Baris Erdem <baris@erdem.dev>
Maintainer profiles
@b-erdem
Licenses
GPL-3.0-only
Website
https://github.com/b-erdem/ml_kem_ada
Repository
github.com/b-erdem/ml_kem_ada
Source revision
0b46ce23243d
Tags
ml-kem, post-quantum, cryptography, spark, embedded, security, verified
Project files
ml_kem_ada.gpr
Manifest
index/ml/ml_kem/ml_kem-1.0.0.toml
Build and platform metadata 1 field
Configuration
{
  "variables": {
    "parameter_set": {
      "default": "ML_KEM_768",
      "type": "Enum",
      "values": [
        "ML_KEM_512",
        "ML_KEM_768",
        "ML_KEM_1024"
      ]
    }
  }
}