WireGuard formal verification, covering aspects of the cryptography, protocol, and implementation

Some good reading here :slight_smile:

And for those wondering when it will come to pfsense they are working on the proper in-kernel implementation and which is better and faster than the potentialy unstable userspace implementations. It’s still progressing well, just not publicly except what can be seen in the code going into FreeBSD directly.

They mentioned in a blog post a few months ago that they are working on it and tracking the verification. And that it was only a matter of time before it is implemented.