This presentation will go over our approach to formal verification of post-quantum cryptographic code at AWS. It will cover our approach to assembly-language

verification, and how we are verifying type-safety of C code within AWS-LC.

Proof also enables "fearless optimization" of crypto code, where proofs of correctness and/or equivalence preserve functional behaviour while allowing and inspiring non-trivial performance improvements. We're also using automated super-optimization of assembly language for our Graviton processors to unlock performance gains on specific micro-architectures.

These technical approaches will be illustrated by the mlkem-native library - an open-source implementation of the recently-standardized MLKEM algorithm that combines formal verification with state-of-the-art performance on all major platforms.