The perturbation project files are held in this folder.

To build the project, run make exe. The resulting executable is stored in ./Scripts/

In order to run the perturber, use the Dafny compiler as normal, but add the --perturbed flag. This will generate perturbed versions of the input program and store them in the same directory as the input program. For example, the command we use is ./Scripts/dafny verify --perturbed <dafny_file>

The dataset we built is formatted as a csv stored here. The CSV has three columns: incorrect_program, verifier_output, and correct_program. The perturbed programs, verifier output, and corresponding correct programs are stored here. We did not verify each perturbed program, so the complete set of perturbed programs we generated are stored here. The correct programs were taken from other Dafny repos, mainly from the libraries repo and this formal verification dataset. The python scripts used to generate and process the perturbed programs are stored here.

We finetuned the OpenLlama3bv2 model using a portion of the data from our dataset. The jupyter notebook for finetuning can be found here. The notebook takes portions of other finetuning scripts from tutorials for single gpu from here and here. The jupyter notebook for playing with the finetuned model can be found here

• better testing infrastructure (we tested using the small programs in the smallTest folder)
• better program slicing
• verify all the perturbed programs
• finetune larger model on larger dataset

Dafny is a verification-ready programming language. As you type in your program, Dafny's verifier constantly looks over your shoulder, flags any errors, shows you counterexamples, and congratulates you when your code matches your specifications. When you're done, Dafny can compile your code to C#, Go, Python, Java, or JavaScript (more to come!), so it can integrate with your existing workflow.

Dafny will give you assurance that your code meets the specifications you write, while letting you write both code and specifications in the Dafny programming language itself. Since verification is an integral part of development, it will thus reduce the risk of costly late-stage bugs that are typically missed by testing.

Dafny has support for common programming concepts such as classes and trait inheritance, inductive datatypes that can have methods and are suitable for pattern matching, lazily unbounded datatypes, subset types e.g. for bounded integers, lambdas, and immutable and mutable data structures.

Dafny also offers an extensive toolbox for mathematical proofs, such as unbounded and bounded quantifiers, calculational proofs, pre- and post-conditions, termination conditions, loop invariants, and read/write specifications.

This github site contains these materials:

• sources
• binary downloads for Windows, macOS, GNU/Linux, and FreeBSD
• the issue tracker
• the wiki, including frequently asked questions

Documentation about the dafny language and tools is located here. A reference manual is available both online and as pdf. (A LaTeX version can be produced if needed.)

You can ask questions about Dafny on Stack Overflow or participate in general discussion on Dafny's .

The easiest way to try out Dafny is to install Dafny on your own machine in Visual Studio Code and follow along with the Dafny tutorial. You can also download and install the Dafny CLI if you prefer to work from the command line.

Here are some ways to get started with Dafny:

• 4-part course on the Basics of specification and verification of code:
  • Lecture 0: Pre- and postconditions (19:08)
  • Lecture 1: Invariants (20:56)
  • Lecture 2: Binary search (21:14)
  • Lecture 3: Dutch National Flag algorithm (20:33)
• New overview article: Accessible Software Verification with Dafny, IEEE Software, Nov/Dec 2017
• Online tutorial, focusing mostly on simple imperative programs
• 3-page tutorial notes with examples (ICSE 2013)
• Dafny Quick Reference
• Language reference for the Dafny type system, which also describes available expressions for each type
• Cheatsheet: basic Dafny syntax on two pages
• Dafny Reference Manual [html] [pdf]
• Dafny libraries, a standard library of useful Dafny functions and lemmas
• Dafny Power User
• Videos at Verification Corner
• Blog

The language itself draws pieces of influence from:

• Euclid (from the mindset of a designing a language whose programs are to be verified),
• Eiffel (like the built-in contract features),
• CLU (like its iterators, and inspiration for the out-parameter syntax),
• Java, C#, and Scala (like the classes and traits, and syntax for functions),
• ML (like the module system, and its functions and inductive datatypes), and
• Coq and VeriFast (like the ability to include co-inductive datatypes and being able to write inductive and co-inductive proofs).

• Haskell-to-Dafny translator, by Duncan White
• Vim-loves-Dafny mode for vim, by Michael Lowell Roberts
• Boogie-Friends Emacs mode

Information and instructions for potential contributors are provided here.

Dafny itself is licensed under the MIT license. (See LICENSE.txt in the root directory for details.) The subdirectory Source/Dafny/Coco contains third party material; see Source/Dafny/Coco/LICENSE.txt for more details.