Comment by lmeyerov

I'm sure it's a pretty good one, but it's quite hard to trust more than that both on the design + impl side if you ever have tried to verify (vs just test) such a system. Think the years of pain for something much more trivial like paxos + an impl of it.

In this case, looks like the community does value backing up its claims, and the protocol is verified: https://www.wireguard.com/formal-verification/ . Pretty awesome! The implementation itself seems to be written unsafely, so TBD there.