First of all congratulations, I do believe that this is good step forwards.

I took a look at the tamarin model, and at least for me it looks pretty much impenetrable (no surprise there). Is it realistic to think that (any?) implementors can use the proven model as the primary reference when implementing the protocol? Especially if you'd strip away the comments, which are not proven to be correct and as such might be misleading?

I'm not extremely experienced in formal verification methods, but isn't usually an implementation that's formally verified? I understand that verifying the protocol is a big deal but if the protocol is not correctly implemented you can't count on any of the promises the protocol makes.

Could you have chosen other provers than Tamarin (which is 100% Haskell for people interested in that) for this job?

If yes, what made you prefer it?

A bit off-topic, but anyone have info about how the move to BSD-compat license went?

Talking about WireGuard... I was just trying to build it a few hours ago, but can’t get it to build against a 4.2.0 kernel :/

Looking at the primitives, isn’t WireGuard effectively using the Noise protocol?