Okay, now you're conflating "verifiability" and "has been verified". One can perfectly build a crypto library with verifiability in mind, then fail to verify some crucial property.
Breaking news: TweetNaCl has not been fully verified. Two instances of Undefined Behaviour (negative left shifts), lines 281 and 685, remain to this date. They're easily found with UBSan (yay for verification!), but for some reason DJB has yet to correct them.
The original paper verified 2 specific memory safety properties (no out of bound accesses, no uninitialised memory access). Monocypher's test suite does the same (and more) on a systematic basis since before version 1.0. I use Valgrind, all sanitizers, and the TIS interpreter. The test suite covers all code & data paths, much thanks to the code being constant time.
So not only Monocypher has been build with verifiability in mind, it has been pretty thoroughly verified. You would know that if the time you took to discredit Monocypher were used to look at it instead. It's all there in tests/test.sh, referenced in the README.
---
About that vulnerability 2 years ago. As shocking at it may be, I learned from it. The looming threat of something similar happening again tends to do that. I've paid my dues since, learned a ton. The audit gives no cause to fear another error of that kind. The test suite was deemed adequate, and they found no bug, however minor.
Breaking news: TweetNaCl has not been fully verified. Two instances of Undefined Behaviour (negative left shifts), lines 281 and 685, remain to this date. They're easily found with UBSan (yay for verification!), but for some reason DJB has yet to correct them.
The original paper verified 2 specific memory safety properties (no out of bound accesses, no uninitialised memory access). Monocypher's test suite does the same (and more) on a systematic basis since before version 1.0. I use Valgrind, all sanitizers, and the TIS interpreter. The test suite covers all code & data paths, much thanks to the code being constant time.
So not only Monocypher has been build with verifiability in mind, it has been pretty thoroughly verified. You would know that if the time you took to discredit Monocypher were used to look at it instead. It's all there in tests/test.sh, referenced in the README.
---
About that vulnerability 2 years ago. As shocking at it may be, I learned from it. The looming threat of something similar happening again tends to do that. I've paid my dues since, learned a ton. The audit gives no cause to fear another error of that kind. The test suite was deemed adequate, and they found no bug, however minor.
That old bug is irrelevant now. Give me a break.