Dafny est outil permettant de faire la preuve automatique de correction d'un programme en utilisant des préconditions et des postconditions. Le langage de programmation de Dafny est inspiré de C#. Un programme Dafny peut traduit automatiquement et compilé vers C#, Java, Javascript, Go, et C++. L'installation la plus simple est via un plugin dans Visual Studio Code.

Plugin Dafny dans Visual Stuio Code