AIAI Seminar: Friday 30th January 2026 by Rod Chapman

Title: Formal is fast: verification and optimization of cryptographic code at AWS

Speaker: Dr Rod Chapman, Senior Principal Applied Scientist, AWS Cryptography

Abstract: This presentation will go over our approach to formal verification of cryptographic code at AWS, concentrating on our recent efforts with ML-KEM and ML-DSA. We'll 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 ML-KEM algorithm that combines formal verification with state-of-the-art performance on all major platforms.

Bio: Rod is a senior principal applied scientist within the Cryptography group of Amazon Web Services. He specializes in the design, development and verification of cryptographic software, and has particular experience with programming language design and automated reasoning technologies. He also coaches development teams and leadership in high-assurance software development disciplines, technologies,

and processes. He is a Fellow of the IET and an honorary visiting professor at the University of York.