High-assurance Post-Quantum Crypto with Franziskus Kiefer and Karthik Bhargavan Security Cryptography Whatever

We welcome Franziskus and Karthik from Cryspen to discuss their new high-assurance implementation of ML-KEM (the final form of Kyber), discussing how formal methods can both help provide correctness guarantees, security assurances, and performance wins for your crypto code!Transcript: https://securitycryptographywhatever.com/2024/01/29/high-assurance-kyber/Links:- https://cryspen.com/post/ml-kem-implementation/- https://github.com/cryspen/libcrux/- https://github.com/formosa-crypto/libjade- h...