Apple today published new corecrypto source code on GitHub, alongside a detailed technical post explaining the intricate work behind its post-quantum cryptography efforts across iPhone, Mac, and more. Here are the details.
Earlier today, Apple published a new corecrypto repository on GitHub as part of a broader update to its post-quantum cryptography work, which started 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 as encryption keys are refreshed over time.
Today’s announcement continues that work, with the GitHub repository including source code for corecrypto, the low-level cryptographic 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 folder.
According to Apple, the latter contains the proof work and supporting tools used to check that its implementations match 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.
Alongside the repository, Apple also published a very detailed look at how it verified this code before making it available for outside review, and why it is releasing today’s material.
With the latest release of corecrypto source code on May 22, 2026, we’re sharing meaningful advances in applied formal verification with the global cryptographic community, including the details of our approach and the tools we used. They are released openly to encourage wider adoption, support critical review of our work, and help advance the state of the art for assuring critical software.
The actual process is incredibly intricate, combining conventional testing, simulation, independent review, 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 has to work across Apple’s product lineup, including devices with different Apple silicon designs. Additionally, Apple’s implementations include both portable C code and hand-optimized ARM64 assembly written to take advantage of its own processors. So, relying on existing verification methods alone wouldn’t cut it.
As Apple explains, this work helped catch issues that conventional testing would not have found before the code reached its products.
For example, we identified a missing step in an early ML-DSA implementation, which in rare cases could cause inputs to exceed the expected range and produce incorrect output. We also discovered an error in a third-party proof, which we were able to independently repair for the specific parameter values used in our implementation. In the worst case scenario, the missing step issue could have silently corrupted cryptographic computations without any warning from existing test suites. Integrating formal verification into our development cycle provided strong assurance that our implementation is correct and that every subroutine works well together.
Finally, the company points to its Formal verification for Apple corecrypto paper (which elaborates on its approach), the custom-built Cryptol-to-Isabelle translator tool (which helps convert part of Apple’s verification work into a format that can be checked against the official standards), and Isabelle theories in the corecrypto source archive (which offer the underlying proof materials experts need to reproduce and evaluate Apple’s results) as supporting materials for security researchers.
You can read the post in Apple’s Security Research blog here, and you can check out the GitHub repository here.
FTC: We use income earning auto affiliate links. More.
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。