I'd rely on this code before I relied on literally any other VPN codebase. Jason should change the wording here, which I think might be old. Like I said: the protocol just got a set of formal proofs, in addition to the Tamarin prover work Jason did for it.
Just because the protocol has a formal set of proofs, doesn't mean it's production ready. The very fact that the only releases are snapshots and not eligible for CVE's makes me weary of utilizing this in a non-testing environment.
But how does a set of proofs let you know that it's not going to cause a kernel panic or stop forwarding traffic in edge-cases that aren't well-tested (e.g. lossy and/or high-latency links).
