[noise] Formal verification of NoiseIK

[Jason A. Donenfeld]

Hey guys,

I'll respond in length soon to the explicit nonce thread. I've been
backed up with the following, but now that this is out of the way I'll
catch up on the other stuff in the list. But first:

https://www.wireguard.io/formal-verification/
https://www.wireguard.io/papers/wireguard-formal-verification.pdf

Nice results for NoiseIK: it isn't terrible!

The paper is still a draft, so if there's something you'd like to see
in it that isn't there, feel free to pipe up.

Jason