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.