🍏 苹果开源 corecrypto 密码库，

🍏 苹果开源 corecrypto 密码库，附形式化验证证明量子安全算法正确性

苹果在 5 月 22 日发布了 corecrypto 源代码，公开了用于对抗未来量子计算机的 ML-KEM 和 ML-DSA 算法实现，并首次提供了端到端的形式化验证数学证明。这些证明确保 C 代码和手工优化的 ARM64 汇编与 NIST 标准严格一致。

量子安全加密已部署于 iMessage、VPN 等场景，而 corecrypto 为超过 25 亿台活跃设备提供基础加密运算。苹果同时公开了定制验证工具和 Isabelle 理论库，供独立专家评估，希望推动关键软件保障技术的进步。

Apple Security Research | Github