Apple today released new corecrypto source code to GitHub, along with a detailed technical article explaining the complex work behind its post-quantum cryptography efforts on iPhone, Mac and more. Here are the details.
Apple continues its post-quantum security work
Earlier today, Apple released a new corecrypto repository on GitHub as part of a broader update to its post-quantum cryptography work, which began rolling out publicly in 2024 with iMessage’s PQ3 protocol.
Announced with iOS 17.4, PQ3 was Apple’s first major public step toward protecting users against future quantum computers, with iMessage adding post-quantum protection both when a conversation starts and when encryption keys are refreshed over time.
Today’s announcement continues this work, with the GitHub repository including the source code for corecrypto, the low-level crypto library used by Apple’s security framework, CryptoKit and CommonCrypto to power encryption, hashing, random number generation and digital signatures.
The repository also includes Apple’s implementations of ML-KEM and ML-DSA (the two post-quantum algorithms the company chose for corecrypto), as well as tests, performance tools, build targets, and a dedicated formal verification file.
According to Apple, the latter contains the proofs and supporting tools used to verify that its implementations meet FIPS 203 and FIPS 204, the NIST standards for ML-KEM (used to help establish secure encryption keys) and ML-DSA (used for digital signatures), designed to protect against known threats posed by future quantum computers.
Apple details its post-quantum security work
Alongside the repository, Apple also released a very detailed look at how it verified this code before making it available for external review, and why it’s releasing today’s material.
With the latest corecrypto source code release on May 22, 2026, we are sharing significant advances in applied formal verification with the global crypto community, including details of our approach and the tools we used. They are published openly to encourage wider adoption, support critical review of our work, and help advance the state of the art in ensuring critical software.
The actual process is incredibly complex, combining conventional testing, simulations, independent reviews, and Apple’s own formal verification work.
Apple says it developed a custom approach because existing tools did not meet all of its requirements, as corecrypto must work across Apple’s entire product line, including devices with different Apple silicon designs. Additionally, Apple’s implementations include both portable C code and manually optimized ARM64 assembly, written to take advantage of its own processors. Thus, relying solely on existing verification methods would not be enough.
As Apple explains, this work helped detect problems that conventional testing would not have detected before the code reached its products.
For example, we identified a missing step in an early implementation of ML-DSA, which in rare cases could cause inputs to exceed the expected range and produce an incorrect result. We also discovered an error in a third-party proof, which we were able to repair independently for the specific parameter values used in our implementation. In the worst case, the missing step issue could have silently corrupted cryptographic calculations without any warning from existing test suites. Incorporating formal verification into our development cycle has provided strong assurance that our implementation is correct and that each subroutine works well together.
Finally, the company points to its formal verification paper for Apple corecrypto (which expands on its approach), the custom Cryptol-to-Isabelle translation tool (which helps convert some of Apple’s verification work into a format that can be verified against official standards), and Isabelle’s theories in the corecrypto source archive (which offer the underlying evidence experts need to reproduce and evaluate Apple’s results) as supports for security researchers.
You can read the article on Apple’s Security Research blog here, and you can view the GitHub repository here.
To discover on Amazon
FTC: We use automatic, revenue-generating affiliate links. More.
