iraca: independent differential verification of ML-KEM (FIPS 203) in RustCrypto | Xiliux Blog

A Rust harness that differences the RustCrypto ml-kem crate (no published audit) against the pq-crystals reference: byte-for-byte identical and rejecting FIPS 203 non-canonical keys, verified by execution.