International Association for Cryptologic Research

International Association
for Cryptologic Research

CryptoDB

Lucas Franceschino

Publications and invited talks

Year
Venue
Title
2025
RWC
Using Formally Verified Post-Quantum Algorithms at Scale
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.