Apple releases post-quantum code on GitHub Apfelpatient

Apple has released new source code for its corecrypto library on GitHub, revealing the foundations of its post-quantum cryptography for iPhone, Mac, and other devices. An accompanying technical article explains how Apple formally verified the correctness of these algorithms - and what flaws were uncovered in the process.

With its release on May 22, 2026, Apple is offering a deeper insight into the encryption architecture of its platforms than ever before. At its core is corecrypto – the cryptographic core library upon which the security frameworks of all Apple devices are built. This initiative continues Apple's unwavering commitment to data privacy, a commitment unmatched by any other major tech company – except that this time the focus is not on end-user features, but on the underlying mathematical foundations.

What Apple specifically released

The new GitHub repository contains the source code of corecrypto, the low-level library that powers Apple's security framework, CryptoKit, and CommonCrypto. It is responsible for encryption, hashing, random number generation, and digital signatures on iPhones, Macs, and all other Apple devices.

Included are Apple's implementations of ML-KEM and ML-DSA, the two post-quantum algorithms that Apple selected for corecrypto. Also included are tests, performance tools, build targets, and a dedicated folder for formal verification. The latter contains the proof-of-concept work and tools that Apple uses to verify that its implementation complies with FIPS 203 and FIPS 204 standards - the NIST standards for ML-KEM and ML-DSA, specifically designed to counter threats from future quantum computers.

ML-KEM serves to securely establish encryption keys, while ML-DSA handles digital signatures.

Background: PQ3 and the Post-Quantum Strategy

Apple's post-quantum work is not new. Back in 2024, the company publicly launched the PQ3 protocol for iMessage, which was introduced with iOS 17.4. PQ3 protects conversations against potential future attacks by quantum computers, both at the start and during regular key renewals.

Apple is thinking long-term: Even if practical quantum computers with sufficient computing power don't yet exist, stored encrypted data could be decrypted in the future as soon as the technology becomes available. This makes current post-quantum protection a preventative measure. Apple's commitment is also evident in its determination not to weaken encryption, even under government pressure – as was recently the case with the British iCloud regulations.

Why Apple developed its own verification tools

In the accompanying technical document, Apple explains why existing verification methods were insufficient. CoreCrypto must function across the entire Apple product range – including various Apple Silicon designs. Furthermore, the implementations include both portable C code and hand-optimized ARM64 assembler specifically tailored for Apple chips.

Apple therefore combines traditional testing, simulation, independent reviews, and its own formal verification work. The latter mathematically checks whether each sub-algorithm does exactly what the standards stipulate.

What the verification has already revealed

Apple explains that formal verification uncovered problems that traditional tests would not have found. An early ML-DSA implementation was missing a processing step - in rare cases, inputs could have exceeded the expected range of values, thus producing incorrect results. Traditional test suites would not have detected the error; in the worst case, the result would have been silently corrupted.

Furthermore, Apple discovered a flaw in a third-party proof approach, which the company was able to correct independently using its own parameters. Both cases demonstrate why Apple considers the additional effort of formal verification necessary.

Disclosure as an invitation to security researchers

Apple also provides a research paper detailing the approach, as well as its proprietary Cryptol-to-Isabelle translation tool and the Isabelle evidence files. These materials allow external experts to independently understand and verify Apple's work.

The release is more than just transparency for PR reasons. Apple is inviting the global crypto community to critically examine what has previously been kept secret. If vulnerabilities are identified early, all Apple devices will ultimately benefit. At the same time, the company is sending a clear signal to an industry where other major platforms are weakening rather than strengthening encryption standards.

Apple's crypto strategy is becoming tangible

This release reveals for the first time the depth of Apple's preparations for the post-quantum era. While end users benefit from PQ3 in iMessage, the methodical hardening of all encryption components continues in the background. The code on GitHub is not just documentation, but an open invitation to participate in the review process – a step that few tech companies take to this extent. (Image: Shutterstock / metamorworks)