One step is making sure that the crypto isn't bogus. That's what this formal verification is about here. The next step would be writing an implementation in a

One step is making sure that the crypto isn't bogus. That's what this formal verification is about here. The next step would be writing an implementation in a language that's verifiable -- such as F* [1] -- 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 [2] [3]. 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. [1] https://www.fstar-lang.org/ https://www.fstar-lang.org/ [2] https://github.com/mitls/hacl-star https://github.com/mitls/hacl-star [3] https://github.com/project-everest/vale https://github.com/project-everest/vale