Mastodon Feed
Reblogged by nadim@infosec.exchange ("Nadim Kobeissi"):
Google adopts @cryspen's formally verified libcrux Rust implementations for ML-KEM and post-quantum algorithms.
“These implementations will be AVX2-optimized, verified in F* and translated into C." for use by Google, and beyond.
Congrats @franziskus & team!
https://bughunters.google.com/blog/6038863069184000/formally-verified-post-quantum-algorithms