There's another paper besides the RHUL one, which preceded it, using tamarin: https://git.zx2c4.com/wireguard-tamarin/tree/wireguard.m4https://www.wireguard.com/papers/wireguard-formal-verificati... There are other groups who are also currently working on similar and better proofs. I think the end goal is to get proofs of the general pattern language of Noise rather than just the WireGuard handshake (IKpsk2), which will probably then satisfy your concerns with Noise. The Noise project itself is also working on things like NoiseSocket which will be more of an easily pluggable "right answer".
Ah cheers for the link. Yeah a proof at the level of abstraction up from a single pattern would be lovely. I don't really have 'concerns' as such: it's just if your risk profile is the thing that has kicked you away from TLS towards Noise then you need a good justification (notwithstanding, a proof of security for a new AKE should really be par for the course).
IMO the interesting aspect with the development of Noise will be if it can avoid bloat. From the mailing list I can see that there's solid awareness of that risk (would assume Trevor is aware anyway), but it will be interesting to see how the simplicity of pattern API will handle things like signatures, when they're inevitably added. I see at least one Noise-using project has already made the leap on that front.
IMO the interesting aspect with the development of Noise will be if it can avoid bloat. From the mailing list I can see that there's solid awareness of that risk (would assume Trevor is aware anyway), but it will be interesting to see how the simplicity of pattern API will handle things like signatures, when they're inevitably added. I see at least one Noise-using project has already made the leap on that front.