A blueprint for formal verification of Apple corecrypto - Apple Security Research<br>Blog

May 22, 2026<br>A blueprint for formal verification of Apple corecrypto<br>Written by Apple Security Engineering and Architecture (SEAR) and Hardware Technologies Formal Verification

The introduction of quantum-secure cryptography in iMessage marked the start of a significant security transition to protect Apple users from threats posed by future quantum computers. Deploying this new generation of algorithms at scale across all Apple platforms requires high assurance, so we developed rigorous new formal verification methods to prove the mathematical correctness of our implementation. With this week’s release of corecrypto, we’re publishing our implementations of quantum-secure ML-KEM and ML-DSA algorithms — along with the mathematical proofs we built to assure they are faithful to the FIPS 203 and FIPS 204 specifications — for independent evaluation by experts. And to further advance the state of the art for assuring critical software, we're also publishing the formal verification libraries and tools that we created to achieve the strongest known correctness results for any widely-deployed production implementation of the relevant algorithms.

In 2024, we added post-quantum encryption to corecrypto, the foundational cryptographic library in Apple operating systems. To address the well-documented threat from future quantum computers, we’ve been working to first develop and deploy strong, quantum-secure cryptography in areas where it’s likely to have the greatest benefit: applications involving encrypted communications and other sensitive information, including iMessage, VPN, and TLS networking. In addition, quantum-secure APIs included with our Apple CryptoKit release last fall enable developers to adopt quantum-secure encryption and authentication in their own apps.

corecrypto is used continuously in our products, providing encryption and decryption, hashing, random number generation, and digital signatures on over 2.5 billion active devices. A critical bug in corecrypto has the potential to compromise the security and reliability of every app and feature that depends on it, so we are conservative when adding new code to the library and make exceptional efforts to be comprehensive in our testing.

We include new cryptographic algorithms in corecrypto only after a thorough assessment against the following criteria:

Improves security . The algorithm must solve new problems or improve on the security of existing algorithms.

Secure design . The algorithm must have strong theoretical security, and must have withstood rigorous, sustained cryptanalysis from the global research community. And practically, it must be feasible to implement the algorithm in a secure way for our intended use.

High performance . Execution must be highly efficient — both in terms of latency and power — as implemented across every Apple device.

Compact parameters . Key sizes, signatures, and ciphertexts must minimize their impact on network latency and fit within device memory constraints.

When an algorithm meets our high bar for inclusion in corecrypto, we develop an implementation that must then be:

Secure . The code must meet exacting security criteria and must not leak information. This requires both correctness and hardening, such as to prevent leaking timing signals that an adversary could use to extract application secrets.

Optimized . The implementation should take maximum advantage of the instructions and architecture of the silicon on which it runs.

Correct . The code, including all relevant optimizations, must faithfully implement the algorithm as defined in the standard which was analyzed by the cryptographic community. It must produce the correct output.

When we evaluated quantum-secure algorithms to include in corecrypto, we quickly converged on two that met our criteria — the same two that would later be selected and standardized by NIST as ML-KEM and ML-DSA (FIPS 203 and FIPS 204, respectively). While NIST also standardized other signature schemes, ML-KEM and ML-DSA best matched our requirements. Significant work by the cryptographic community had produced reference implementations for ML-KEM and ML-DSA that, in our own evaluation, showed a strong foundation of security and performance.

Because corecrypto is used across Apple products — including specialized chips with different microarchitectures — we start by writing our algorithm implementations in portable C code. To ensure the implementations run correctly and securely wherever corecrypto is deployed, our guidelines are strict: we write this code to avoid leaking secret values through execution timing, prevent the compiler from inadvertently weakening those protections, and take advantage of hardware features like Data Independent Timing (DIT) and Pointer Authentication (PAC) on Apple processors, which respectively guard against a range of micro-architectural side channels...