Written by Apple Security Engineering and Architecture (SEAR) and Hardware Technologies Formal VerificationThe introduction of quantum-secure cryptography in iMessage marked the start of a significant security transition to protect Apple users from threats posed by future quantum computers. Deploying this new generation of algorithms at scale across all Apple platforms requires high assurance, so we developed rigorous new formal verification methods to prove the mathematical correctness of our i...