Understanding lattice risks: Many differences between marketing and reality

For a counterpoint Sophie Schmieg recently wrote https://keymaterial.net/2026/06/18/on-hybrid-signatures/ arguing against hybrids. Putting EC and PQ algorithms together isn't trivial, and the complexity of using multiple algorithms in parallel can, itself, lead to more issues.

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

This is a dense article but what seems reasonably clear is that someone is pushing hard for an insecure standard.

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.

I have no horses in this race and lack the expertise to judge, but this is part of a larger fight and djb seems to be on the other side of a lot of good cryptographers:

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