形式化验证
WireGuard 经过了各种形式化验证，涵盖了加密、协议和实现的各个方面。下面详细介绍了各项努力。
使用 Tamarin 对协议进行符号验证
技术论文中描述的基于Noise的WireGuard 协议已使用Tamarin在符号模型中进行了形式化验证。这意味着 WireGuard 协议具有安全性证明。该协议已被验证具有以下安全属性：
- 正确性
- 强密钥一致性和真实性
- 抵御密钥泄露冒充
- 抵御未知密钥共享攻击
- 密钥保密
- 前向保密
- 会话唯一性
- 身份隐藏
这是 Jason Donenfeld 和 Kevin Milner 的合作作品。
这些结果在 WireGuard 形式化验证论文中得到了广泛的讨论。这篇论文是一份正在进行的草稿，但主要结果已经在那里了。
狨猴模型
Tamarin 模型是开源的，可以重新运行进行独立验证：
$ git clone https://git.zx2c4.com/wireguard-tamarin/
$ cd wireguard-tamarin
$ make
eCK 模型中协议的计算证明
在尝试在 eCK 模型中构建 WireGuard 的计算证明时，结果发现 WireGuard 协议并不完全适合传统的 eCK 模型，因为密钥确认消息是传输层的一部分。因此，本文证明了 WireGuard 协议的一个变体，它在道德上与实际协议等同，并得出了非常有力的结果。
这是 Benjamin Dowling 和 Kenneth G. Paterson 的合作作品。
ACCE 模型中的协议计算证明
本论文使用CryptoVerif在类似 ACCE 的计算模型中构建了整个 WireGuard 协议（包括传输数据消息）的机械化加密证明。证明的属性包括：
- 正确性
- 消息保密
- 前向保密
- 相互认证
- 抵御密钥泄露冒充
- 抵御未知密钥共享攻击
- 第一个协议消息的抗重放性
该模型可供下载，并可在 CryptoVerif 2.00 中使用。
这是 Benjamin Lipp 的作品。
使用 ProVerif 对协议进行符号验证
Noise Explorer项目旨在通过生成ProVerif模型来正式验证所有Noise 协议模式。与 WireGuard 相关的模型是Noise Explorer 的 IK 模型，该模型可以插入 ProVerif 以生成各种属性的证明。
这是 Nadim Kobeissi 和 Karthikeyan Bhargavan 的作品。
Curve25519 的已验证 C 实现
HACL*
WireGuard makes use of HACL*'s 64-bit Curve25519 scalar multiplication implementation. The curve is specified in F*, which is then able to prove things about implementation strategies. KreMLin lowers it down to verified C.
HACL* is joint work of Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche.
Fiat-Crypto
WireGuard also makes use of Fiat-Crypto's 32-bit Curve25519 scalar multiplication implementation. The curve is specified in Coq, which is then able to prove things about implementation strategies and emit verified C.
Fiat-Crypto is joint work of Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala.