Security4 min read
Apple Publishes Formally Verified Quantum-Secure Cryptographic Algorithms in corecrypto
Tags Infrastructure · Enterprise
Apple Security Research·
Apple has published formally verified implementations of ML-KEM (FIPS 203) and ML-DSA (FIPS 204) quantum-secure algorithms in corecrypto, along with mathematical proofs and verification tools. Apple claims the strongest known correctness results for any widely-deployed production implementation of these post-quantum algorithms. The formal verification libraries and tools are being released as open source.
Technical significance
Formal verification of production-grade post-quantum cryptography at this scale sets a new bar for the industry. As NIST's post-quantum migration deadline (2030) approaches, Apple's approach — publishing proofs and tools — could become a template for other platform vendors preparing for quantum threats.