Ce projet rassemble des analyses symboliques du protocole WireGuard à l'aide d'assistants de preuve comme Tamarin, ProVerif et Sapic+. Il vérifie des propriétés de sécurité telles que l'accord, le secret et l'anonymat, et propose des correctifs pour améliorer ces propriétés. Les résultats sont obtenus via des modèles formels et des évaluations automatisées.