International Association
for Cryptologic Research

In an attempt to provide organizations with access to correct and bug-free implementations of the new NIST-selected PQC algorithms, Cryspen and Google have joined forces to produce formally verified, open source implementations of these algorithms. In this talk we will cover our cutting-edge approach to formally verifying ML-KEM, the challenges encountered during the verification process, and the timing side channel attack uncovered by the process. We will also discuss the way forward for formal verification of PQC algorithms, the impact of formal verification on the development workflow, and the subsequent deployment of secure and optimized PQC implementations.