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?
However, if you actually read the Tamarin manual -- the documentation is really terrific -- I think you'll find that the spthy code quickly comes into focus as something very straight-forward.
So much so, in fact, that I'd really recommend fluency with something like Tamarin as an essential thing for anybody working on crypto things, even if they're not in academia. It should be accessible to folks who describe themselves as "crypto engineers." Next time you find yourself having to work on or analyze a custom crypto protocol, give it a shot.
The next step would be writing an implementation in a language that's verifiable -- such as F*  -- and then using that to output actually verified binaries. People are indeed working on this kind of thing, to the point where even the primitives are being generated in this way, such as the HACL* and Vale projects  . These are in service of making a verified TLS stack. It's nicely modularized and some of this might, at some point in time, be used for a verified WireGuard implementation. Or, alternatively, other unrelated methods for that. These are exciting times in the formal methods space.
In any case, this paper is about the first -- and incredibly important -- step of that kind of journey: making sure the crypto constructions WireGuard uses are top notch and actually has the super strong security properties we want it to have.
I want to describe (at a more abstract level) a protocol (this allows anyone to implement a specific instance of it in their language or platform of choice). For that you use a formal specification language (Z Notation, Event-B, TLA+, etc.). These lend themselves to formal analysis (evaluation of the specification via standard logic or temporal logic; modeling of the specification for violations of invariants and constraints).
If the protocol specification has been verified, you can then be more confident that an implementation of that protocol specification is correct (in principle) and then set about verifying the implementation via either more formal methods (static analysis tools, SPARK, Eiffel's contracts, Frama-C, etc.) or testing (more likely some degree of both). And if you have a formal specification you may be able to construct a better test set than the ad hoc test set usually constructed by developers and testers for systems (that is, it'll be constructed systematically and thoroughly; not haphazardly or just by collecting all the previous PR tests together for regression testing). If, for instance, you have a set of invariants for your system and guards for all your actions, you can construct tests which specifically attempt to violate these (or do violate them and see how your system reacts).
If yes, what made you prefer it?
Also I think part of the power in using Tamarin is that if it's having trouble proving something automatically, it's easy to jump in and try to prove it manually with a relatively straightforward graphical representation of the trace sets. That also helps you spot any potential interim properties you might need to prove as helper lemmas, etc.
It's gotten some recent popularity for the work on TLS 1.3 as well , and with that an effort to improve the materials available for people to pick it up themselves [1, 2]. Some of the things we did to nudge Tamarin's heuristic in the right direction when autoproving the WireGuard model (documented in the .m4 file) are getting baked in to Tamarin soon.
(For what it's worth, you don't actually have to deal with any Haskell unless you're planning on modifying the prover, the protocol models are in their own language.)
Looking at the primitives, isn’t WireGuard effectively using the Noise protocol?
Yes, WireGuard uses Noise, plus other things. For more information, there's the WireGuard paper .
jfyi, that is the error the build is failing on: /tmp/WireGuard-0.0.20170706/src/receive.c:225:4: error: too few arguments to function ‘IP6_ECN_set_ce’
I didn't want to discredit the WireGuard protocol - it was just something that came to my mind when looking at the primitives. Thanks for your work
Regarding building on 4.2.0; you should make sure it's a real 4.2.0 and not your distro's 4.2.0. I was shocked to see how many non-stability, non-security patches are backported by distro kernels. The package could say 4.2.0, but since 4.2 was never an upstream LTS release, it's likely that it's a frankenkernel. Because distro kernels often misrepresent the version, it seems like a real pain to keep DKMS working on them.
I will try to build a newer one. Thanks for your input!