There’s no reason at this point to put all your cryptographic eggs in the post-quantum crypto (PQC) basket. Elliptic curve crypto (ECC) is widely studied and understood; while it’s more vulnerable to quantum cryptanalysis, this is mitigated by the hybrid ECC+PQC proposals (except a bit of lost performance). On the flip side, the PQC stuff is new enough that new attacks are still being devised, so relying fully on that seems like a bad idea. Someone is trying to force the standardization of a PQC-only standard under the claim that it is secure enough, but ignores evidence from quite recent work showing that attacks continue to improve. This is before getting into the fact that PQC implementations are harder to get right and that popular PQC implementations have had nasty side-channel attacks.

In response to the implementation errors in ML-KEM, companies have moved to formal verification. Apple, for example, recently released[1] a formally verified ML-KEM implementation, where they formally verified the assembly of the implementation to verify that it matches the specification and that it's side-channel free. AWS, similarly, is using a formally verified ML-KEM implementation: "All AArch64 and x86_64 assembly is proved to be functionally correct, memory-safe, and of secret-independent timing (constant-time)" [2].

There are similar efforts (by both Apple, Amazon, and others) to formally prove ML-DSA implementations as well.

[1]: https://security.apple.com/blog/formal-verification-corecryp... [2]: https://github.com/pq-code-package/mlkem-native

https://mailarchive.ietf.org/arch/msg/tls/ZBpcicZX1Dxnam2gMa...