• feat: Dafny now has partial support for compiling programs to Python (#1871, #1886, #1891, #1928, #1973, #1979, #2031, #2081)
• feat: The synthesize attribute on methods with no body allows synthesizing objects based on method postconditions at compile time (currently only available for C#). See Section 22.2.20 of the Reference Manual. (#1809)
• feat: The /verificationLogger:text option now prints all verification results in a human-readable form, including a description of each assertion in the program.
• feat: The /randomSeedIterations:<n> option (from Boogie) now tries to prove each verification condition n times with a different random seed each time, to help efficiently and conveniently measure the stability of verification. (boogie-org/boogie#567)
• feat: The new /runAllTests can be used to execute all methods with the {:test} attribute, without depending on a testing framework in the target language.
• feat: Recognize !in operator when looking for compilable comprehensions (#1939)
• feat: The Dafny language server now returns expressions ranges instead of token ranges to better report errors (#1985)
• fix: Miscompilation due to incorrect parenthesization in C# output for casts. (#1908)
• fix: Populate TestResult.ResourceCount in /verificationLogger:csv output correctly when verification condition splitting occurs (e.g. when using /vcsSplitOnEveryAssert).
• fix: DafnyOptions.Compiler was null, preventing instantiation of ModuleExportDecl (#1933)
• fix: /showSnippets crashes Dafny's legacy server (#1970)
• fix: Don't check for name collisions in modules that are not compiled (#1998)
• fix: Allow datatype update expressions for constructors with nameonly parameters (#1949)
• fix: Fix malformed Java code generated for comprehensions that use maps (#1939)
• fix: Comprehensions with nested subset types fully supported, subtype is correctly checked (#1997)
• fix: Fix induction hypothesis generated for lemmas with a receiver parameter (#2002)
• fix: Make verifier understand (!new) (#1935)
• feat: Some command-line options can now be applied to individual modules, using the {:options} attribute. (#2073)
• fix: Missing subset type check in datatype updates (#2059)
• fix: Fix initialization of non-auto-init in-parameters in C#/JavaScript/Go compilers (#1935)
• fix: Resolution of static functions-by-method (#2023)
• fix: Export sets did not work with inner modules (#2025)
• fix: Prevent refinements from changing datatype and newtype definitions (#2038)
• feat: The new older modifier on arguments to predicates indicates that a predicate ensures the allocatedness of some of its arguments. This allows more functions to show that their quantifiers do not depend on the allocation state. For more information, see the reference manual section on older. (#1936)
• fix: Fix (!new) checks (#1419)
• fix: multiset keyword no longer crashes the parser (#2079)