Verified Post-Quantum Crypto on the Web

Want to Learn More?

Here are some blog posts to start you off:

• Formally Verified Post-Quantum Cryptography
• Verified ML-KEM (Kyber) in Rust
• Verifying Libcrux's ML-KEM
• High Assurance IoT PQC
• Google Bug Hunters: Formally Verified Post-Quantum Algorithms
• Google Security Blog: A new path for Kyber on the web

Here are some technical references:

• Internet-Draft: Post-quantum hybrid ECDHE-MLKEM Key Agreement for TLSv1.3
• Firefox 132.0 Release Notes
• Cloudflare Research: Post-Quantum Key Agreement (similar to this page)