At the upcoming International Cryptographic Module Conference 2026, Nicky Mouha, Founder of KeyCryptic, will speak about something that sounds straightforward but rarely is: assuring that cryptographic algorithms are implemented correctly.
His talk, “Understanding Formal Verification: Lessons from Verifying Post-Quantum-Secure Implementations,” will focus on mlkem-native and mldsa-native. These are high-performance implementations of post-quantum algorithms, consisting of C code proven free of memory and integer overflows, and assembly verified for correctness and constant-time behavior. They are widely deployed in practice, for example, in AWS-LC and liboqs.
In this case, the selected verification approach did not detect certain integer overflows, and will go into details of where the discrepancies occurred. The talk will emphasize that no vulnerabilities were found, and that the issues were already acknowledged and addressed by the project maintainers.
As post-quantum cryptography is deployed more widely, these implementation details are becoming increasingly important.
The session takes place on Tuesday, April 21, 2026, at 13:30.