How Amazon Verifies and Optimizes Post-Quantum Cryptography

RSA and ECC could be broken once quantum computers become powerful enough. That's why, to prepare against store-now-decrypt-later attacks—where encrypted data is stored today and decrypted later—organizations need to transition to post-quantum cryptography (PQC) in advance.

Amazon built mlkem-native, an open-source implementation targeting NIST's FIPS-203 standard, ML-KEM, that satisfies both formal verification and performance optimization at the same time. The goal was to increase security without compromising customer experience or maintainability.

The key was combining simple C reference code with research-grade optimization techniques into a single production codebase. To do this, Amazon adopted a modular structure where the frontend handles ML-KEM's high-level logic and the backend handles performance-sensitive computation. Backends for AArch64, x86_64, and RISC-V64, along with a base C implementation, are all provided, so architecture-specific fast paths can be added while preserving the overall structure.

Verification proceeds along two tracks.

• CBMC is used to prove memory safety and type safety of the C code.
• Machine/human-readable contracts are attached to each function to automatically confirm the absence of buffer overflows and arithmetic overflows.

In particular, ML-KEM's lazy modular arithmetic requires precisely tracking worst-case bounds to ensure values never exceed the 16-bit integer range. Since worst-case bounds—not average values—must be the basis for this, manual review is slow and error-prone. CBMC automates this bound tracking, ensuring safety even in complex low-level arithmetic.

For the most performance-critical parts, Keccak and NTT, hand-written optimized assembly was used, but verification was not abandoned. Amazon uses SLOTHY to optimize microarchitecture-specific scheduling and register allocation, and uses HOL Light and s2n-bignum to prove the functional correctness of the AArch64 and x86_64 assembly. Even when re-optimized with SLOTHY, the proofs remain independent of instruction ordering and register allocation, so performance improvements don't add to the verification burden.

Transparency is also emphasized. SOUNDNESS.md documents what has been proven, what has been assumed, and what risks remain. The verification tools and artifacts are also open-sourced, allowing external parties to reproduce the same conclusions.

The results are clear. mlkem-native has been integrated into AWS-LC, and on EC2 instances, operations per second increased by 2.0x to 2.4x compared to the reference implementation. In conclusion, Amazon has demonstrated that formal verification, optimization, and maintainability are goals that don't have to conflict with one another.