Formally Verified Post-Quantum Cryptography at Scale

ABSTRACT

The transition to post-quantum cryptography presents a critical verification challenge: how do we deliver implementations that are simultaneously optimized for production performance and formally verified for correctness? This talk presents our experience developing, optimizing, and formally verifying ML-KEM (Module-Lattice-Based Key-Encapsulation Mechanism) for AWS-LC, Amazon's cryptographic library powering billions of daily operations across security-critical AWS services. 

Our implementation, developed as the open-source 'mlkem-native' project under the Post-Quantum Cryptography Alliance, achieves 2.08x-2.78x performance improvements on Graviton processors and 1.5x-2.0x on x86 processors compared to previous implementations, while maintaining formal correctness guarantees. The AArch64 assembly is super-optimized using SLOTHY - a constraint solving super-optimizer - yet remains fully verified for functional correctness.

We focus particularly on our HOL Light verification methodology for hand-crafted assembly code, building on the s2n-bignum verification infrastructure previously used for other cryptographic primitives such as RSA and ECC. We describe the challenges of verifying super-optimized assembly, our approach to structuring proofs that track optimized code through CI pipelines, and our ongoing work proving constant-time execution properties. Complementing this, all C code is verified for memory- and type-safety using CBMC, using contracts and loop invariants to provide sound, unbounded and modular verification.

One of the key enablers of this verification effort was our use of NeuroSymbolic AI techniques to accelerate proof engineering. We employed AI to generate comprehensive documentation of HOL Light proof tactics and then leveraged this documentation to help propose proof strategies for our verification goals. This combination of rigorous formal methods with AI-assisted proof discovery illustrates a practical path toward scaling formal verification to production cryptographic code. Furthermore, having established strong formal guarantees of correctness (so called “guardrails”) in CI, we have been using AI systems to assist with refactoring and improvement of the codebase with some success. The trick is that the verification flow is so fast that the AI engines can iterate and repair verification failures as they go along.

We share lessons learned from integrating this verified implementation into AWS-LC's FIPS validation cycle, and reflect on how this model of rapid open-source development followed by verified integration is shaping our approach to the future development of AWS-LC.

BIO

Dusan Kostic is an applied scientist in AWS Cryptography and a core developer and maintainer of AWS-LC, Amazon's general-purpose cryptographic library. His work focuses on post-quantum cryptography, the PQ transition within AWS, and formal verification of cryptographic algorithm implementations. More recently, Dusan has been exploring the use of AI to assist with formal proof development for cryptographic algorithms, as well as AI-assisted code review and vulnerability scanning of cryptographic codebases.