mlkem-native

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, A