{
  "$type": "site.standard.document",
  "bskyPostRef": {
    "cid": "bafyreichryhdwmyadxj7xgp65ebt3gsavf5boblbvu62ozwnzb6f3siqlq",
    "uri": "at://did:plc:awj2q63kg2v3k5xwsjh2uoe3/app.bsky.feed.post/3mmuvt4kf4ci2"
  },
  "coverImage": {
    "$type": "blob",
    "ref": {
      "$link": "bafkreie3khx2towm2564fzgv3gsm756xqlmxdordyit5g6p7wj6jyglr7u"
    },
    "mimeType": "image/jpeg",
    "size": 137143
  },
  "description": "Apple has published the source code for their corecrypto libraries on GitHub, along with the tools and formal verification libraries they used to evaluate their cryptography, so independent cryptography experts can verify it for themselves.",
  "path": "/news/2026/05/28/apple-publishes-source-code-for-their-cryptography-on-github/",
  "publishedAt": "2026-05-28T01:49:57.000Z",
  "site": "https://www.privacyguides.org",
  "tags": [
    "published",
    "GitHub page",
    "License.txt",
    "Open Source Initiative"
  ],
  "textContent": "Apple has published the source code for their `corecrypto` libraries on GitHub, along with the tools and formal verification libraries they used to evaluate their cryptography, so independent cryptography experts can verify it for themselves.\n\n`corecrypto` is, like the name suggests, the core of Apple's cryptography, providing \"encryption and decryption, hashing, random number generation, and digital signatures on over 2.5 billion active devices.\"\n\nAs such, it's important to ensure their encryption behaves the way it's supposed to.\n\nBy using mathematical proofs, Apple claims it can \"show that our algorithm implementations are correct to a significantly greater degree of assurance than conventional software testing allows.\"\n\nThey say that using formal verification, they caught issues that would have slipped by otherwise:\n\n> . . . we believe the types of subtle issues that we found and fixed can be uncovered only with formal methods. And while we focused our formal verification work on functional correctness, we also used extensive conventional testing, including simulation tools to cover other aspects of our implementation, such as protection against information leakage. Based on our work to date, we believe that the strongest assurance possible comes from combining formal verification with conventional methods and critically evaluating the end-to-end results.\n\nApple does lay out some limitations of their formal verification. For example, they assume that the compiler behaves correctly.\n\nStill, it seems like they believe they've really made some strides in formal verification, and cryptography experts can verify themselves.\n\nAnyone interested in cryptography or formal verification can check out the new GitHub page and play around with the tooling.\n\nIt's important to note that, while the source code for `corecrypto` is public, it's not open source software, since you aren't allowed to freely redistribute or modify the software:\n\n> The publication of this code is primarily intended for security research and verification purposes. The default license for the corecrypto (cc) project is the evaluation-only corecrypto Internal Use License Agreement contained in License.txt.\n\nThe license doesn't meet the requirements of open source software, as defined by the Open Source Initiative.\n\nHowever, all the security benefits of public access to the source code apply. Anyone is free to analyze it themselves for bugs or errors.\n\nHopefully more projects like WhatsApp publish the source code and formal verification tooling for their cryptography.",
  "title": "Apple Publishes Source Code for Their Cryptography on GitHub",
  "updatedAt": "2026-05-28T01:49:57.724Z"
}