Apple open-sources quantum-resistant encryption code

Apple published implementations of quantum-resistant algorithms (ML-KEM and ML-DSA), along with formal verification tools, libraries, and documentation used to mathematically prove correctness; these are integrated into its corecrypto library and have been deployed in iMessage, VPN and TLS. The formal verification process found a potential ML-DSA signing bug that would have impacted authentication if it reached production, and Apple recommends a hybrid approach combining formal proofs with conventional testing for robust assurance.