A differential and adversarial verification harness for post-quantum cryptography: it compares an implementation against independent references by feeding the same deterministic bytes, and tests the input validation the standard requires. Today it differences RustCrypto's ml-kem against three implementations (pq-crystals C, libcrux and AWS-LC) and its ml-dsa against dilithium.

Why three implementations and not one?

Because a single oracle can share the blind spot of the code it measures. Three independent implementations —one in another language, one formally verified, one production-hardened— almost never share the same bug; all four agreeing bit for bit is a far stronger signal.

Did you find a bug in RustCrypto?

No. This is an assurance result: RustCrypto passes the verified conformance checks. It is a conformance spot-check, not a full audit, and it does not cover side channels.

Is this useful for my post-quantum implementation?

Yes: the harness can difference your implementation against independent references and test its input validation, with positive controls and red/green pairs.

iraca: differential verification of ML-KEM and ML-DSA against three independent implementations

What we did

iraca is a harness that verifies the post-quantum cryptography the Rust ecosystem actually ships, by differencing it against independent implementations. The widely-used RustCrypto ml-kem crate (ML-KEM / FIPS 203), which has no published independent audit, is byte-for-byte identical to three implementations that do not know each other: the pq-crystals C reference, libcrux (from Cryspen, formally verified) and AWS-LC (Amazon's production library). They agree on key generation, encapsulation and decapsulation, across all three levels —ML-KEM-512, 768 and 1024.

The same harness differences ML-DSA (FIPS 204, the signature) at its three levels —44, 65 and 87— against the dilithium reference, byte for byte, with cross-verification.

This is a conformance spot-check, not a full audit, and it does not cover side channels (the KyberSlash class).

Why it matters

The NIST standards (FIPS 203/204/205) are final and migration is mandated. Much of the Rust world uses the RustCrypto crates, which today have no independent audit. And a single oracle can share the blind spot of the code it measures. Three independent implementations —one in a different language, one formally verified, one hardened for production— close that gap: all four agreeing bit for bit is a far stronger signal than agreeing with one.

The method: the same raw bytes to every side

iraca feeds the same bytes to the crate and to each oracle through their deterministic entry points, with no DRBG and no .rsp replay. With determinism end to end, any disagreement is a real one, not randomness noise. The C references (pq-crystals and AWS-LC) are compiled from source and linked behind a thin FFI module; libcrux is a Rust dependency; everything else is safe Rust.

An adversarial layer also tests input validation: in ML-KEM it generates non-canonical encapsulation keys (a coefficient greater than or equal to q) and checks the reject that FIPS 203 requires (the modulus check); in ML-DSA it tests the hint-padding canonicity FIPS 204 requires. The oracle for canonicity is the standard itself, not another implementation.

Results

ML-KEM-512/768/1024 (four-way): keys, ciphertexts and shared secrets byte-for-byte identical across RustCrypto, pq-crystals, libcrux and AWS-LC, over 128 seeds per level plus a fixed vector.
ML-DSA-44/65/87 (two-way): byte-for-byte agreement with the dilithium reference on key and deterministic signature, with cross-verification (each side accepts the other's signature) and the adversarial hint-canonicity layer.
Adversarial conformance: RustCrypto rejects the non-canonical inputs the standards require, confirmed by reading the source and by execution.

Every result ships a red/green pair and a positive control. A no-disagreement result only counts if the comparison path actually ran and can discriminate: we proved it by flipping one byte in each implementation and watching the bench go red.

What it is not

Not a full audit; not side-channel or timing analysis; one version and a few concrete properties. Assurance is cumulative, not a single stamp.

Reproducible, and open to collaboration

The harness is small, deterministic and built to be re-run. If you maintain a post-quantum implementation and want an independent differential and adversarial pass, or an oracle to diff your own work against, that is what it is for. I also work with the Ethereum Foundation's post-quantum effort on signature-scheme verification.