Overview
- Apple published its ML-KEM and ML-DSA implementations and the associated formal verification artifacts on May 22, 2026 to allow independent researchers to inspect and reuse the work.
- The company released a custom verification pipeline built with Galois that uses Cryptol, a Cryptol-to-Isabelle translator, SAW, and the Isabelle proof assistant to show implementations match NIST-aligned specifications.
- Formal verification uncovered and led Apple to fix subtle errors that normal testing missed, including a missing computational step in an early ML-DSA implementation that could silently produce incorrect signatures.
- Apple proved both portable C code and hand-optimized ARM64 assembly for Apple Silicon against the formal models to preserve performance and reduce timing risks, while still relying on testing for parts that tools cannot fully verify.
- Because corecrypto runs across billions of devices and supports iMessage, VPN and TLS, the release aims to raise industry confidence in post-quantum rollouts and invite external review that could speed broader adoption and harden implementations.