A blueprint for formal verification of Apple corecrypto
Summary
Apple outlines a formal verification-driven approach for corecrypto, validating ML-KEM and ML-DSA implementations with Isabelle, SAW, Cryptol, and custom tooling. The post describes portable C and ARM64 verification, extensive subroutine proofs, and a combined use of formal methods with conventional testing to strengthen cryptographic software assurance.