How much of the development of this was verified, and what does that consist of?
I worry a little when I read that things are verified and were hard.
How much of the development of this was verified, and what does that consist of?
I worry a little when I read that things are verified and were hard.
https://eprint.iacr.org/2017/536.pdf is the relevant paper that introduces the project and its broad design. Figure 1 on page 3 is a good place to look.
The first two shouldn't matter because the entirety of the code is verified and anyone can check the verification. The last is an issue with any cryptography but verification doesn't try to address that only that the code does precisely and only what it's supposed to; ie it should guarantee that there are no exploits possible against that library.