logoalt Hacker News

A blueprint for formal verification of Apple corecrypto

51 pointsby hasheddanyesterday at 6:52 PM1 commentview on HN

Comments

H0-LawJikyesterday at 11:06 PM

The missing-step bug in early ML-DSA is the perfect case for SAW. rare inputs that pass code review because the line that should be there doesn't look absent, it looks like the next line is correct. tests wouldn't catch it unless someone happened to roll exactly the right inputs.