Thomas Bosboom ✅Apple published a detailed write-up on formal verification in corecrypto, including their ML-KEM and ML-DSA implementations for post-quantum cryptography.
This goes to the next level, beyond “we tested this carefully” to “we proved key parts equivalent to the FIPS specs, including optimized C and ARM64 assembly paths.”
This crypto library ships across billions of devices. This is the difficult, expensive assurance work that makes platform security real. https://security.apple.com/blog/formal-verification-corecrypto/ #AppleSecurity #Cryptography #PostQuantum #InfoSec
A blueprint for formal verification of Apple corecrypto - Apple Security Research
With the latest release of corecrypto, we’re publishing our implementations of quantum-secure ML-KEM and ML-DSA algorithms, along with the mathematical proofs we built to assure they are faithful to the FIPS 203 and FIPS 204 specifications. To advance the state of the art for assuring critical software, we're also publishing the formal verification libraries and tools that we created to achieve the strongest known correctness results for any widely-deployed production implementation of the relevant algorithms.