Dafny is a programming language with a program verifier. As you type in your program, the verifier constantly looks over your shoulders and flags any errors.
- Compile and run
- Automatic installation of the newest Dafny version.
- Automatic verification as one types.
- Errors, warnings and hints are shown through the VSCode interface.
- When there are no errors, you get a 👍 on the status bar.
- Syntax highlighting thanks to sublime-dafny. See file
- Display counter example for failing proof.
- IntelliSense for classes and CodeLens showing method references.
On the first start the plugin asks you to install Dafny automatically.
Add null check
Some diagnostics can be directly inserted with a quickfix at the beginning of a line.
Compile and Run
Show Counter Example