Apple has published the formal verification results for its implementations of the ML-KEM and ML-DSA algorithms

The company's specialists presented the formal verification results for their implementations of post-quantum–resistant algorithms ML-KEM and ML-DSA, designed to protect users across Apple's ecosystem from threats posed by quantum computers.

Formal verification is the mathematical validation of a system or implementation to demonstrate that it satisfies specific, predefined properties.

Apple and Galois engineers used reference algorithm implementations as a baseline, developed optimized versions, and performed formal verification to confirm that the modifications did not affect the correctness of their outputs. For instance, during the analysis of the ML-DSA assembly implementation for Apple Silicon processors, the team discovered a bug — a missing step in an early version — that conventional software testing had not detected.

Technical details of the verification process are provided in "Formal verification for Apple corecrypto: ML-KEM and ML-DSA in 2026". Part of the verification toolkit has been released publicly, along with the corecrypto library source code, which is used throughout the Apple ecosystem.

The ML-KEM and ML-DSA implementations were included in the May 22 release of the corecrypto library, and with Apple CryptoKit support, third-party developers can now integrate them into their own applications.

💬 Discuss