There's also a formal proof of Wireguard's security (not that it means much in practice, but I find it extremely interesting): https://prosecco.gforge.inria.fr/

There's also a formal proof of Wireguard's security (not that it means much in practice, but I find it extremely interesting): https://prosecco.gforge.inria.fr/personal/bblanche/publications/LippBlanchetBhargavanEuroSP19.pdf https://prosecco.gforge.inria.fr/personal/bblanche/publicati...