Why3 est une plateforme pour la vérification déductive de programmes. Elle fournit un langage riche pour la spécification et la programmation, appelé WhyML, et s'appuie sur des preuves externes, automatisées et interactives, pour prouver les conditions de vérification. Why3 dispose d'une bibliothèque standard de théories logiques et de structures de données de base telles que des tableaux, des files d'attente et des tables de hachage.