You'd be surprised how many of those submitted and approved crypto standards are still not tested with industry best practices.
buffer overflows or integer UB's and overflows are very common.
ubsan, asan, valgrind tests are missing. some do offer symbolic verification of the algo, but not the implementations.
Proof of constant-time execution is an interesting field, but as I understand very much less mature than the SPARK toolset. If anyone has a toolchain working over llvm to check and/or make code constant-time, I'm interested.
I mean, if the standards people want to keep writing C, they can probably use Frama-C for the standard implementation...
buffer overflows or integer UB's and overflows are very common. ubsan, asan, valgrind tests are missing. some do offer symbolic verification of the algo, but not the implementations.
See my https://github.com/rurban/smhasher#crypto paragraph, and "Finding Bugs in Cryptographic Hash Function Implementations", Nicky Mouha, Mohammad S Raunak, D. Richard Kuhn, and Raghu Kacker, 2017. https://eprint.iacr.org/2017/891.pdf