Upcoming

May 13, 2026 · View on GitHub

See docs/dev/news/.

4.11.0

New features

  • Stabilize verifications by automatically computing triggers for the quantified proof obligations associated with :| constructs. Manually specified triggers and warning-suppressing attributes are also supported (and mentioned in warning messages, as for other quantifiers and comprehensions).

    Enhance witness guessing for the proof obligation associated for :| assignments. (https://github.com/dafny-lang/dafny/pull/6023)

  • Four new Dafny standard libraries:

    • Std.Actions - utilities for abstract imperative actions, including enumerating and streaming values
    • Std.Frames - utilities related to working with dynamic framing, often related to reads and modifies clauses
    • Std.Ordinal - operations and properties of the ORDINAL type
    • Std.Termination - a datatype for representing Dafny decreases clauses and extensions (https://github.com/dafny-lang/dafny/pull/6074)

  • Support using --standard-libraries with --enforce-determinism. Removed Std.Collections.Seq.SetToSeq since it was slow and not compatible with this mode. (https://github.com/dafny-lang/dafny/pull/6137)

  • With --standard-libraries you can now read UTF-8 text files from the disk using Std.FileIO.ReadUTF8FromFile(path: string): Result<string, string>. To write some content to the disk, use Std.FileIO.WriteUTF8ToFile(path: string, content: string): Outcome<string>. Standard library breaking change: All UnicodeEncodingForm versions of FromUTF8Checked, FromUTF16Checked and DecodeCodeUnitSequenceChecked now return a Result instead of an Option so that the error message is clearer. Migration is easy: Use .ToOption() if you really prefer an option. Affected refining modules: Utf8EncodingForm and Utf16EncodingForm (https://github.com/dafny-lang/dafny/pull/6198)

  • The Dafny standard libraries now include a powerful parser combinators framework, available through Std.Parsers.StringBuilders.

    Key Features

    • Guaranteed Termination: All parsers, including those built with recursive combinators, are proven to terminate
    • Mutual Recursion Support: Build complex parsers that can reference each other (demonstrated in the Polynomial example)
    • Rich Error Reporting: Failed parsing attempts combine their error messages to provide meaningful feedback
    • Developer-Friendly Tools: Built-in debugging utilities for inspecting parser inputs and outputs
    • Memory-Efficient Recursion: Advanced implementations avoid stack overflow in recursive parsers
    • Elegant DSL: Compact, datatype-based combinators designed for readability and composition
    • Flexible Backtracking: Optional backtracking available through .??() (DSL) or ?(...) (standard syntax)
    • Comprehensive Toolkit: Rich set of combinators including lookahead, negation, folding, and binding operations
    • The library includes several practical examples, including JSON and SMT parsers, each implemented in about 50 lines of code. (https://github.com/dafny-lang/dafny/pull/6243)

  • Dafny classes and traits can now redeclare methods defined by traits they inherit from. (https://github.com/dafny-lang/dafny/pull/6280)

  • Real literals now support scientific notation using lowercase e to denote the exponent (like 1.23e5 for 123000.0 or 5e-2 for 0.05). Real literals also support convenient trailing-dot shorthand (like 1. for 1.0) and leading-dot shorthand (like .5 for 0.5 or .5e2 for 50.0). Note that explicit + signs in exponents are not supported; use 5e2 instead of 5e+2. (https://github.com/dafny-lang/dafny/pull/6286)

Bug fixes

4.10.0

New features

  • Support for code actions in the language server to:

    • Insert failing implicit assertions in a "by" clause by preference.
    • Insert forall statement for any forall expressions that could not be proved
    • Insert calc statement for any equality that cannot be proved. (https://github.com/dafny-lang/dafny/pull/6044)

  • Besides --filter-position :<line>, also support --filter-position :<start>-<end>, --filter-position :<start>- and --filter-position :-<end> (https://github.com/dafny-lang/dafny/pull/6077)

  • The option --iterations for the command measure-complexity, has been renamed to --mutations. The option --progress VerificationJob has been renamed to --progress Batch. (https://github.com/dafny-lang/dafny/pull/6078)

Bug fixes

4.9.1

New features

  • Introduce the attributes {:isolate} and {:isolate "paths} that simplify the verification of an assertion by introducing additional verification jobs. {:isolate} can be applied to assert, return and continue statements. When using {:isolate_assertions} or --isolate-assertions, each return statement now creates a separate verification job for each ensures clause. Previously all ensures clauses where verified in a single job, for all return statements. (https://github.com/dafny-lang/dafny/pull/5832)

  • Fill in matching patterns for the quantifiers introduced by automatic induction to represent the induction hypothesis. Suppress the generation of the induction hypothesis if no such matching patterns are found. Enhance tooltips accordingly. This feature is added to stabilize verification, but by sometimes not generating induction hypotheses, some automatic proofs may no longer go through. For backward compatibility, use an explicit {:induction ...} where ... is the list of variables to use for the induction-hypothesis quantifier. Additionally, use a {:nowarn} attribute to suppress any warning about lack of matching patterns.

    Improve the selection of induction variables.

    Allow codatatype equality in matching patterns and as a focal predicate for extreme predicates.

    More specifically:

    • If a lemma bears {:induction x, y, z}, where x, y, z is a subset of the lemma's parameters (in the same order that the lemma gives them), then an induction hypothesis (IH) is generated. The IH quantifies over the given variables.

      For an instance-member lemma, the variables may include the implicit this parameter.

      For an extreme lemma, the IH generated is the for corresponding prefix lemma, and the given variables may include the implicit parameter _k.

      If good matching patterns are found for the quantifier, then these are indicated in tooltips. If no patterns are found, then a warning is generated; except, if the lemma bears {:nowarn}, then only an informational message is given.

    • If a lemma bears {:induction} or {:induction true}, then a list of induction variables is determined heuristically.

      If the list is empty, then a warning message is generated and no IH is generated. If the list is nonempty, an IH is generated and the list of variables is indicated in a tooltip.

      If good matching patterns are found for the quantifier, then these are indicated in tooltips. If no patterns are found, then a warning is generated; except, if the lemma bears {:nowarn}, then only an informational message is given.

    • If a lemma bears {:induction false}, then no IH is generated.

    • If a lemma bears an :induction attribute other than those listed above, then an error is generated.

    • If a lemma bears no :induction attribute, and the --manual-lemma-induction flag is present, then no IH is generated.

    • Otherwise, a list of induction variables is determined heuristically.

      If this list is empty, then no IH is generated and no warning/info is given.

      If the list is nonempty, then the machinery looks for matching patterns for the IH quantifier. If none are found, then no IH is generated. An informational message is generated, saying which candidate variables were used and saying that no matching patterns were found.

      If patterns are found, then an IH is generated, the list of variables and the patterns are indicated in tooltips, and the patterns are used with the IH quantifier.

      The pattern search can be overridden by providing patterns explicitly using the {:inductionTrigger} attribute. This attribute has the same syntax as the {:trigger} attribute. Using an empty list of triggers restores Dafny's legacy behavior (no triggers for lemma induction hypotheses). (https://github.com/dafny-lang/dafny/pull/5835)

  • Accept decreases to and nonincreases to expressions with 0 LHSs and/or 0 RHSs, and allow parentheses to be omitted when there is 1 LHS and 1 RHS. (https://github.com/dafny-lang/dafny/pull/5891)

  • Allow forall statements in statement expressions (https://github.com/dafny-lang/dafny/pull/5894)

  • When using --isolate-assertions or {:isolate_assertions}, a separate assertion batch will be generated per pair of return statement and ensures clause. (https://github.com/dafny-lang/dafny/pull/5917)

Bug fixes

4.9.0

New features

Bug fixes

4.8.1

New features

  • feat: allow type parameters of newtype declarations feat: support optional witness clause of constraint-less newtype declarations feat: show tool tips for auto-completed type parameters feat: show tool tips for inferred (==) characteristics fix: Don't let newtype well-formedness checking affect witness checking (fixes ##5520) fix: Check the emptiness status of constraint-less newtype declarations (fixes #5521) (https://github.com/dafny-lang/dafny/pull/5495)

  • New feature: model extractor

    CLI option

    The dafny verify command now has an option --extract:<file>, where (just like for the various print options) <file> is allowed to be - to denote standard output.

    Extract mechanism

    Upon successful verification, the new extract mechanism visits the AST of the given program. For any module marked with {:extract}, the extract-worthy material from the module is output. The output declarations will be in the same order as they appear textually in the module (in particular, the fact that module-level Dafny declarations are collected in an internal class _default has no bearing on the output order).

    Three kinds of declarations are extract-worthy:

    • A type declaration A<X, Y, Z> that bears an attribute {:extract_name B} is extracted into a Boogie type declaration type B _ _ _;.

      The definition of the type is ignored. (The intended usage for an extracted type is that the Dafny program give a definition for the type, which goes to show the existence of such a type.)

    • A function declaration F(x: X, y: Y): Z that bears an attribute {:extract_name G} is extracted into a Boogie function declaration function G(x: X, y: Y): Z;.

      The body of the Dafny function is ignored. (The intended usage for an extracted function is that the Dafny program give a definition for the function, which goes to show the existence of such a function.)

    • A lemma declaration L(x: X, y: Y) requires P ensures Q that bears an attribute {:extract_pattern ...} or an attribute {:extract_used_by ...} is extracted into a Boogie axiom. The axiom has the basic form axiom (forall x: X, y: Y :: P ==> Q);.

      If the lemma has an attribute {:extract_used_by F}, then the axiom will be emitted into the uses clause of the Boogie function generated for Dafny function F.

      If the lemma has no in-parameters, the axiom is just P ==> Q.

      If the lemma has in-parameters, then any attribute {:extract_pattern E, F, G} adds a matching pattern { E, F, G } to the emitted quantifier. Also, any attribute {:extract_attribute "name", E, F, G} adds an attribute {:name E, F, G} to the quantifier.

    Expressions

    The pre- and postconditions of extracted lemmas turn into analogous Boogie expressions, and the types of function/lemma parameters and bound variables are extracted into analogous Boogie types. The intended usage of the extract mechanism is that these expressions and types do indeed have analogous Boogie types.

    At this time, only a limited set of expressions and types are supported, but more can be added in the future.

    Any forall and exists quantifiers in expressions are allowed to use :extract_pattern and :extract_attribute attributes, as described above for lemmas.

    Some extracted expressions are simplified. For example, true && !!P is simplified to P.

    Soundness

    The Dafny program that is used as input for the extraction is treated like any other Dafny program. The intended usage of the extraction mechanism is to prove parts of the axiomatization in DafnyPrelude.bpl to be logically consistent. Whether or not the extracted Boogie declarations meet this goal depends on the given Dafny program. For example, if the given Dafny program formalizes sequences in terms of maps and formalizes maps in terms of sequences, then the extraction probably does not provide guarantees of consistency. (https://github.com/dafny-lang/dafny/pull/5621)

  • Dafny-to-Rust: {:test} methods generate #[test] wrappers in Rust that can be invoked using cargo test. Similarly, {:rust_cfg_test} on modules generates a #[cfg(test)] in the resulting rust module. (https://github.com/dafny-lang/dafny/pull/5676)

Bug fixes

4.8.0

New features

  • Introduce hide statements that enable hiding the body of a function at a particular proof location, which allows simplifying the verification of that proof in case the body of the function is not needed for the proof. Hide statements make the opaque keyword on functions obsolete. (https://github.com/dafny-lang/dafny/pull/5562)

  • Let the command measure-complexity output which verification tasks performed the worst in terms of resource count. Output looks like: ... Verification task on line 8 in file measure-complexity.dfy consumed 9984 resources Verification task on line 7 in file measure-complexity.dfy consumed 9065 resources ... (https://github.com/dafny-lang/dafny/pull/5631)

  • Enable the option --enforce-determinism for the commands resolve and verify (https://github.com/dafny-lang/dafny/pull/5632)

  • Method calls get an optional by-proof that hides the precondition and its proof (https://github.com/dafny-lang/dafny/pull/5662)

Bug fixes

4.7.0

New features

  • Add the option --find-project that given a Dafny file traverses up the file tree until it finds a Dafny project that includes that path. This is useful when developing a particular file and doing CLI invocations as part of your development workflow.

  • Improved error reporting when verification times out or runs out of resources, so that when using --isolate-assertions, the error message points to the problematic assertion. (https://github.com/dafny-lang/dafny/pull/5281)

  • Support newtypes based on map and imap (https://github.com/dafny-lang/dafny/pull/5175)

  • To enable smoothly working with multiple projects inside a single repository, Dafny now allows using a Dafny project file as an argument to --library. When using dafny verify, Dafny ensures that any dependencies specified through a project are verified as well, unless using the flag --dont-verify-dependencies. (https://github.com/dafny-lang/dafny/pull/5297)

  • Experimental Dafny-to-Rust compiler development

  • Allow for plugins to add custom request handlers to the language server. (https://github.com/dafny-lang/dafny/pull/5161)

  • Deprecated the unicode-char option (https://github.com/dafny-lang/dafny/pull/5302)

  • Warn when passing a Dafny source file to --library (https://github.com/dafny-lang/dafny/pull/5313)

  • Add support for "translation records", which record the options used when translating library code.

    • --translation-record - Provides a .dtr file from a previous translation of library code. Can be specified multiple times.
    • --translation-record-output - Customizes where to write the translation record for the current translation. Defaults to the output directory. Providing translation records is necessary to handle options such as --outer-module that affect how code is translated. (https://github.com/dafny-lang/dafny/pull/5346)

  • The new decreases to expression makes it possible to write an explicit assertion equivalent to the internal check Dafny does to prove that a loop or recursive call terminates. (https://github.com/dafny-lang/dafny/pull/5367)

  • The new assigned expression makes it possible to explicitly assert that a variable, constant, out-parameter, or object field is definitely assigned. (https://github.com/dafny-lang/dafny/pull/5501)

  • Greatly reduced the size of generated code for the backends: C#, Python, GoLang and JavaScript.

  • Introduce additional warnings that previously only appeared when running the dafny audit command. Two warnings are as follows:

    • Emit a warning when exporting a declaration that has requires clauses or subset type inputs
    • Emit a warning when importing a declaration that has ensures clauses or subset type outputs Those two can be silenced with the flag --allow-external-contracts. A third new warning occurs when using bodyless functions marked with {:extern}, and can be silenced using the option --allow-external-function.

  • Enable project files to specify another project file as a base, which copies all configuration from that base file. More information can be found in the reference manual.

Bug fixes

4.6.0

New features

Bug fixes

4.5.0

New features

  • Add the option --include-test-runner to dafny translate, to enable getting the same result as dafny test when doing manual compilation. (https://github.com/dafny-lang/dafny/pull/3818)

    • Fix: verification in the IDE no longer fails for iterators
    • Fix: the IDE now provides feedback when verification fails to run, for example due to a bad solver path
    • Fix: let the IDE correctly use the solver-path option when it's specified in a project file
    • Feat: improve the order of verification diagnostics emitted by the Dafny CLI, so that they now always follow the line order of the program. (https://github.com/dafny-lang/dafny/pull/4798)
    • Add an option --filter-position to the dafny verify command. The option filters what gets verified based on a source location. The location is specified as a file path suffix, optionally followed by a colon and a line number. For example, dafny verify dfyconfig.toml --filter-position=source1.dfy:5 will only verify things that range over line 5 in the file source1.dfy. In combination with ``--isolate-assertions, individual assertions can be verified by filtering on the line that contains them. When processing a single file, the filename can be skipped, for example: dafny verify MyFile.dfy --filter-position=:23`
    • Add an option --filter-symbol to the dafny verify command, that only verifies symbols whose fully qualified name contains the given argument. For example, dafny verify dfyconfig.toml --filter-symbol=MyModule will verify everything inside MyModule.
    • The option --boogie-filter has been removed in favor of --filter-symbol (https://github.com/dafny-lang/dafny/pull/4816)

  • Add a json format to those supported by --log-format and /verificationLogger, for producing thorough, machine readable logs of verification results. (https://github.com/dafny-lang/dafny/pull/4951)

    • Flip the behavior of --warn-deprecation and change the name to --allow-deprecation, so the default is now false, which is standard for boolean options.
    • When using --allow-deprecation, deprecated code is shown using tooltips in the IDE, and on the CLI when using --show-tooltips.
    • Replace the option --warn-as-error with the option --allow-warnings. The new option, when false, the default value, causes Dafny to stop generating executable output and return a failure exit code, when warnings occur in the program. Contrary to the previous --warn-as-error option, warnings are always reported as warnings.
      • During development, users must use dafny run --allow-warnings if they want to run their Dafny code when it contains warnings.
      • If users have builds that were passing with warnings, they have to add --allow-warnings to allow them to still pass.
      • If users upgrade to a new Dafny version, and are not using --allow-warnings, and do not want to migrate off of deprecated features, they will have to use --allow-deprecation.
    • When using the legacy CLI, the option /warningsAsErrors now has the behavior of --allow-warnings=false
    • A doo file that was created using --allow-warnings causes a warning if used by a consumer that does not use it. (https://github.com/dafny-lang/dafny/pull/4971)

  • The new {:contradiction} attribute can be placed on an assert statement to indicate that it forms part of an intentional proof by contradiction and therefore shouldn't be warned about when --warn-contradictory-assumptions is turned on. (https://github.com/dafny-lang/dafny/pull/5001)

  • Function and method parameters and return types, and datatype constructor arguments, can now have attributes. By default, there are no attributes that Dafny recognizes in these positions, but custom back-ends can use this feature to get extra information from the source files. (https://github.com/dafny-lang/dafny/pull/5032)

  • Under the CLI option --general-newtypes, the base type of a newtype declaration can now be (int or real, as before, or) bool, char, or a bitvector type.

    as and is expressions now support more types than before. In addition, run-time type tests are supported for is expressions, provided type parameters are injective (as was already required) and provided the constraints of any subset type or newtype is compilable. Note, although both as and is allow many more useful cases than before, using --general-newtypes will also forbid some unusual cases that were previously allowed. Any such case that is now forbidden can still be done by doing the as/is via int. (https://github.com/dafny-lang/dafny/pull/5061)

  • Allow newtype declarations to be based on set/iset/multiset/seq. (https://github.com/dafny-lang/dafny/pull/5133)

Bug fixes

4.4.0

New features

  • Reads clauses on method declarations are now supported when the --reads-clauses-on-methods option is provided. The {:concurrent} attribute now verifies that the reads and modifies clauses are empty instead of generating an auditor warning. (https://github.com/dafny-lang/dafny/pull/4440)

  • Added two new options, --warn-contradictory-assumptions and --warn-redundant-assumptions, to detect potential problems with specifications that indicate that successful verification may be misleading. These options are currently hidden because they may occasionally produce false positives in cases where proofs are so trivial that the solver never does work on them. (https://github.com/dafny-lang/dafny/pull/4542)

  • Verification of the {:concurrent} attribute on methods now allows non-empty reads and modifies clauses with the {:assume_concurrent} attribute. (https://github.com/dafny-lang/dafny/pull/4563)

  • Implemented support for workspace/symbol request to allow IDE navigation by symbol. (https://github.com/dafny-lang/dafny/pull/4619)

  • The new --verification-coverage-report flag to dafny verify creates an HTML report highlighting which portions of the program were and were not necessary for verification. The format is the same as for dafny generate-tests --coverage-report and files from the two commands can be merged. (https://github.com/dafny-lang/dafny/pull/4625)

  • Built-in types such as the nat subset type, tuples, arrows, and arrays are now pre-compiled into each backend's runtime library, instead of emitted on every call to dafny translate, to avoid potential duplicate definitions when translating components separately. (https://github.com/dafny-lang/dafny/pull/4658)

  • The new --only-label option to merge-coverage-reports includes only one category of highlighting in the output. For example, merging coverage reports from test generation and verification using the option --only-label NotCovered will highlight only the regions not covered by either testing or verification. (https://github.com/dafny-lang/dafny/pull/4673)

  • The Dafny distribution now includes standard libraries, available with the --standard-libraries option. See https://github.com/dafny-lang/dafny/blob/master/Source/DafnyStandardLibraries/README.md for details. (https://github.com/dafny-lang/dafny/pull/4678)

  • Introduce replaceable modules, which can be used to help define Dafny applications that translate to multiple target languages. (https://github.com/dafny-lang/dafny/pull/4681)

  • The new --coverage-report flag to dafny run and dafny test creates an HTML report highlighting which portions of the program were executed at runtime. (https://github.com/dafny-lang/dafny/pull/4755)

  • Enable turning nonlinear arithmetic on or off on a per-module basis, using the attribute {:disable-nonlinear-arithmetic}, which optionally takes the value false to enable nonlinear arithmetic. (https://github.com/dafny-lang/dafny/pull/4773)

  • Let the IDE provide code navigation in situations where the program parses but has resolution errors. Note that this only works for modules whose dependency tree does not have errors, or modules who contain errors themselves, but not for modules whose dependencies contain errors. (https://github.com/dafny-lang/dafny/pull/4855)

Bug fixes

4.3.0

New features

  • Add support for the Find References LSP request

  • Improve scalability of inlining for test generation and generate coverage information with respect to the original Dafny source (https://github.com/dafny-lang/dafny/pull/4255)

  • Support generating of tests targeting path-coverage of the entire program and tests targeting call-graph-sensitive block coverage (referred to as Branch coverage) (https://github.com/dafny-lang/dafny/pull/4326)

  • Add support for Rename LSP request

  • Make verification in the IDE more responsive by starting verification after translating the required module to Boogie, instead of first translating all modules that could be verified. (https://github.com/dafny-lang/dafny/pull/4378)

  • The Dafny IDE now has improved behavior when working with a Dafny file that's part of a Dafny project. A Dafny file is part of a project if a dfyconfig.toml can be found somewhere in the file's path hierarchy, such as in the same folder or in the parent folder. A dfyconfig.toml can specify which Dafny options to use for that project, and can specify which Dafny files are part of the project. By default, the project will include all .dfy files reachable from the folder in which the dfyconfig.toml resides. Project related features of the IDE are:

    • Whenever one file in the project is opened, diagnostics for all files in the Dafny project are shown. When including a file with errors that's part of the same project, the message "the included file contains errors" is no longer shown. Instead, the included file's errors are shown directly.
    • If any file in the project is changed, diagnostics for all files in the project are updated. Without a project, changing an included file will not update diagnostics for the including file until the including file is also changed.
    • The find references feature (also added in this release), works better in files that are part of a project, since only then can it find references that are inside files that include the current file.
    • The assisted rename feature (also added in this release), only works for files that are part of a project.
    • When using a project file, it is no longer necessary to use include directives. In the previous version of Dafny, it was already the case that the Dafny CLI, when passed a Dafny project file, does not require include directives to process the Dafny program. The same now holds for the Dafny IDE when working with Dafny files for which a project file can be found.
    • If any file in the project is resolved, all files in the project are resolved. Opening a file in a project that's already resolved means the opened file is resolved instantly.
    • The IDE's memory consumption stays the same regardless of how many files in a project are opened. Without a project, the IDE increases its memory usage for each open file.

    Try out the IDE's project support now by creating an empty dfyconfig.toml file in the root of your project repository. (https://github.com/dafny-lang/dafny/pull/4435)

  • Prior to generating tests, Dafny now checks the targeted program for any features that test generation does not support or any misuse of test generation specific attributes. Any such issues are reported to the user. (https://github.com/dafny-lang/dafny/pull/4444)

  • Added documentation of the generate-tests command to the reference manual (https://github.com/dafny-lang/dafny/pull/4445)

  • When two modules in the same scope have the same name, Dafny now reports an error that contains the location of both modules. (https://github.com/dafny-lang/dafny/pull/4499)

    • The Dafny IDE will now report errors that occur in project files.
    • The Dafny IDE will now shown a hint diagnostic at the top of Dafny project files, that says which files are referenced by the project. (https://github.com/dafny-lang/dafny/pull/4539)

Bug fixes

4.2.0

New features

Bug fixes

4.1.0

New features

  • Added support for .toml based Dafny project files. For now the project file only allows specifying which Dafny files to include and exclude, and what options to use. The CLI commands that take Dafny files as input, such as build, run, translate, will now also accept Dafny project files. When using an IDE based on dafny server, such as the Dafny VSCode extension, the IDE will look for a Dafny project file by traversing up the file tree from the currently opened file, until it finds it dfyconfig.toml. The project file will override options specified in the IDE. (https://github.com/dafny-lang/dafny/pull/2907)

  • Recognize the {:only} attribute on assert statements to temporarily transform other assertions into assumptions (https://github.com/dafny-lang/dafny/pull/3095)

  • Exposes the --output and --spill-translation options for the dafny test command (https://github.com/dafny-lang/dafny/pull/3612)

  • The dafny audit command now reports instances of the {:concurrent} attribute, intended to flag code that is intended, but can't be proven, to be safe for use in a concurrent setting. (https://github.com/dafny-lang/dafny/pull/3660)

  • Added option --no-verify for language server (https://github.com/dafny-lang/dafny/pull/3732)

  • Documenting Dafny Entities

    • Added .GetDocstring(DafnyOptions) to every AST node
    • Plugin support for custom Docstring formatter,
    • Activatable plugin to support a subset of Javadoc through --javadoclike-docstring-plugin
    • Support for displaying docstring in VSCode (https://github.com/dafny-lang/dafny/pull/3756)

  • Documentation of the syntax for docstrings added to the reference manual (https://github.com/dafny-lang/dafny/pull/3773)

  • Labelled assertions and requires in functions (https://github.com/dafny-lang/dafny/pull/3804)

  • API support for obtaining the Dafny expression that is being checked by each assertion (https://github.com/dafny-lang/dafny/pull/3888)

  • Added a "Dafny Library" backend, which produces self-contained, pre-verified .doo files ideal for distributing shared libraries. .doo files are produced with commands of the form dafny build -t:lib .... (https://github.com/dafny-lang/dafny/pull/3913)

  • Semantic interpretation of dots in names for {:extern} modules when compiling to Python (https://github.com/dafny-lang/dafny/pull/3919)

  • Code actions in editor to explicit failing assertions. In VSCode, place the cursor on a failing assertion that support being made explicit and either

    • Position the caret on a failing assertion, press CTRL+; and then ENTER
    • Hover over the failing division by zero, click "quick fix", press ENTER Both scenarios will explicit the failing assertion. If you don't see a quick fix, it means that the assertion cannot be automatically made explicit for now.

    Here is a initial list of assertions that can now be made explicit:

    • Division by zero
    • "out of bound" on sequences index, sequence slices, or array index
    • "Not in domain" on maps
    • "Could not prove unicity" of var x :| ... statement
    • "Could not prove existence" of var x :| ... statement (https://github.com/dafny-lang/dafny/pull/3940)

Bug fixes

4.0.0

Breaking changes

3.13.1

New features

Bug fixes

3.12.0

New features

Bug fixes

3.11.0

New features

  • Go to definition now works reliably across all Dafny language constructs and across files. (https://github.com/dafny-lang/dafny/pull/2734)

  • Improve performance of Go code by using native byte/char arrays (https://github.com/dafny-lang/dafny/pull/2818)

  • Introduce the experimental measure-complexity command, whose output can be fed to the Dafny report generator. In a future update, we expect to merge the functionality of the report generator into this command. (https://github.com/dafny-lang/dafny/pull/3061)

  • Integrate the Dafny auditor plugin as a built-in dafny audit command. (https://github.com/dafny-lang/dafny/pull/3175)

  • Add the --solver-path option to allow customizing the SMT solver used when using the new Dafny CLI user interface. (https://github.com/dafny-lang/dafny/pull/3184)

  • Add the experimental --test-assumptions option to all execution commands: run, build, translate and test. When turned on, inserts runtime tests at locations where (implicit) assumptions occur, such as when calling or being called by external code and when using assume statements. Functionality is still being expanded. Currently only checks contracts on every call to a function or method marked with the {:extern} attribute. (https://github.com/dafny-lang/dafny/pull/3185)

  • For the command translate, renamed the option --target into language and turned it into a mandatory argument. (https://github.com/dafny-lang/dafny/pull/3239)

  • Havoc assignments now count as assignments for definite-assignment checks. (https://github.com/dafny-lang/dafny/pull/3311)

  • Unless --enforce-determinism is used, no errors are given for arrays that are allocated without being initialized. (https://github.com/dafny-lang/dafny/pull/3311)

  • Enable passing a percentage value to the --cores option, to use a percentage of the total number of logical cores on the machine for verification. (https://github.com/dafny-lang/dafny/pull/3357)

  • dafny build for Java now creates a library or executable jar file.

    • If there is a Main method, the jar is an executable jar. So a simple A.dfy can be built as dafny build -t:java A.dfy and then run as java -jar A.jar
    • If there is no Main entry point, all the generated class files are assembled into a library jar file that can be used on a classpath as a java library.
    • In both cases, the DafnyRuntime library is included in the generated jar.
    • In old and new CLIs, the default location and name of the jar file is the name of the first dfy file, with the extension changed
    • In old and new CLIs, the path and name of the output jar file can be given by the --output option, with .jar added if necessary
    • As before, the compilation artifacts (.java and .class files) are placed in a directory whose name is the same as the jar file but without the .jar extension and with '-java' appended
    • With the new CLI, the generated .java artifacts are deleted unless --spill-translation=true and the .class files are deleted in any case; both kinds of files are retained with the legacy CLI for backwards compatibility.
    • If any other jar files are needed to compile the dafny/java program, they must be on the CLASSPATH; the same CLASSPATH used to compile the program is needed to run the program

    Having a library or executable jar simplifies the user's task in figuring out how to use the built artifacts. (https://github.com/dafny-lang/dafny/pull/3355)

Bug fixes

3.10.0

New features

Bug fixes

3.9.1

New features

Bug fixes

3.9.0

3.8.1

3.8.0

3.7.3

  • feat: Less code navigation when verifying code: In the IDE, failing postconditions and preconditions error messages now immediately display the sub-conditions that Dafny could not prove. Both on hover and in the Problems window. (https://github.com/dafny-lang/dafny/pull/2434)
  • feat: Whitespaces and comments are kept in relevant parts of the AST (https://github.com/dafny-lang/dafny/pull/1801)
  • fix: NuGet packages no longer depend on specific patch releases of the .NET frameworks.

3.7.2

3.7.1

3.7.0

3.6.0

3.5.0

3.4.2

3.4.1

3.4

  • For certain classes of changes to a Dafny program, prevent unexpected changes in verification behavior.
  • Add command line options to assist in debugging verification performance.
  • Critical fixes to the IDE and greatly improved responsiveness of non-verification IDE features.
  • The C# back-end supports traits as type parameters on datatypes.

Verification

  • feat: Prevent changes in the verification behavior of a proof, when any of these types of changes are made to Dafny user code:

    • Changes to declarations not referenced by the method being verified
    • Changes to the name of any declaration
    • Changes to the order of top-level declarations

  • feat: Assist in debugging the verification performance of a proof by adding the /vcsSplitOnEveryAssert CLI option and {:vcs_split_on_every_assert} attribute (see https://github.com/boogie-org/boogie/issues/465), and report the outcome and duration of splits when they occur in /verificationLogger:trx content.

  • feat: Add a /verificationLogger:csv CLI option that emits the same status and timing information as /verificationLogger:trx, but in an easier-to-parse format, along with Z3 resource counts for more repeatable tracking of verification difficulty.

  • fix: Resolve unsoundness issue (https://github.com/dafny-lang/dafny/issues/1619).

  • fix: Don't silently succeed if the solver crashes (https://github.com/boogie-org/boogie/pull/488).

IDE

  • feat: Verification status reporting shows which proof is being verified, which can help debug slow to verify proofs.

  • feat: Publish parsing and resolution diagnostics before verification has completed. Verification diagnostics from previous runs are migrated.

  • feat: Enable 'go to definition', 'hover' and 'signature help' features before verification has completed.

  • feat: Improve the hover feature to work for a wider scope of Dafny constructs, including function and method parameters, forall, exists and let expressions, and set and map comprehensions.

  • feat: Add an experimental verification caching feature, which enables automatically determining which proofs need to verify again after making changes.

  • feat: Display related resolution errors using nested diagnostics instead of independent diagnostics.

  • fix: Clean up process resources if IDE closed or restarted.

  • fix: Do not let the Dafny compilation status bar get in a stuck state.

UX

  • feat: Improve error reporting when providing incorrectly typed arguments in a function call.
  • feat: Improve error reporting when using type tests.

C#

Various improvements

  • fix: DafnyLanguageServer.dll and Dafny.dll depended on two different versions of Newtonsoft.Json, which could cause crashes in development environments.
  • fix: (error reporting) Types with the same name but from different modules are now disambiguated in error messages.
  • fix: (error reporting) Messages about arguments / parameters type mismatch are clearer and include the parameter name if available.
  • fix: (robustness) Exceptions during parsing, if any, won't crash the language server anymore.
  • fix: The elephant operator (:-) has a clearer error message and no longer reject generic methods on its right-hand side.

Breaking changes

  • The verifier in Dafny 3.4 is now more efficient for many programs, and making changes to Dafny programs is less likely to cause verification to take longer or timeout. However, it is still possible for some correct programs to take longer to verify than on Dafny 3.3, or for verification to fail. For users with such programs who are not yet ready to modify them to pass the 3.4 verifier, we offer the command line option /mimicVerificationOf:3.3 to keep the Dafny 3.4 verification behavior consistent with 3.3.

  • In Dafny 3.3, comprehensions quantified over subset types did not validate the constraint of the subset type, which could result in crashes at run-time. In 3.4, subset types are disabled in set comprehensions in compiled contexts, unless the subset constraint is itself compilable.

    Before, the following code would pass Dafny and be compiled without error, but would crash at run-time:

    type RefinedData = x: Data | ghostFunction(x)
method Main() {
  var s: set<Data> = ...
  var t = set x: RefinedData | x in s;
  forall x in t {
    if !ghostFunction(x) {
      var crash := 1/0;
    }
  }
}

    In Dafny 3.4, the same code triggers a resolution error of the form:

    Error: RefinedData is a subset type and its constraint is not compilable, hence it cannot yet be used as the type of a bound variable in set comprehension. The next error will explain why the constraint is not compilable.
Error: ghost constants are allowed only in specification contexts

  • Changes in type inference may cause some programs to need manual type annotations. For example, in the nested pattern in the following program

    datatype X<+T> = X(x: T)
datatype Y<T> = Y(y: T)

function method M(): (r: X<Y<nat>>) {
    var d: X<Y<int>> := X(Y(3));
    match d
    case X(Y(i)) => X(Y(i))
}

    the type of the Y constructor needs the type to be given explicitly X(Y<nat>.Y(i). As a variation of that program

    datatype X<+T> = X(x: T)
datatype Y<T> = Y(y: T)

trait Tr {}
class Cl extends Tr {
    constructor () {}
}

method M() returns (r: X<Y<Cl>>) {
    var cl := new Cl();
    var d: X<Y<Tr>> := X(Y(cl));
    match d
    case X(Y(tr)) => r := X(Y(tr));
}

    the program can be specified with an explicit cast X(Y(tr as Cl)).