Apple publishes formal verification framework for post‑quantum corecrypto
Apple announced the integration of post‑quantum ML‑KEM and ML‑DSA algorithms into its corecrypto library and released the C and ARM64 implementations along with full formal verification proofs against FIPS 203/204. The company also open‑sourced the verification libraries and tools used to certify the correctness of the widely‑deployed cryptographic code.