• feat: Introduce a new Dafny CLI UI that complies with the POSIX standard and uses verbs to distinguish between use-cases. Run the Dafny CLI without arguments to view help for this new UI. (#2823)
• feat: Support for testing certain contracts at runtime with a new /testContracts flag (#2712)
• feat: Support for parsing Basic Multilingual Plane characters from UTF-8 in code and comments (#2717)
• feat: Command-line arguments are now available from Main in Dafny programs, using Main(args: seq<string>) (#2594)
• feat: Generate warning when 'old' has no effect (#2610)
• fix: Missing related position in failing precondition (#2658)
• fix: No more IDE crashing on the elephant operator (#2668)
• fix: Use the right comparison operators for bitvectors in Javascript (#2716)
• fix: Retain non-method-body block statements when cloning abstract signatures (#2731)
• fix: Correctly substitute variables introduced by a binding guard (#2745)
• fix: The CLI no longer attempts to load each DLL file passed to it. (#2568)
• fix: Improved hints and error messages regarding variance/cardinality preservation (#2774)
• feat: New behavior for import opened M where M contains a top-level declaration M, see PR for a full description (#2355)
• fix: The DafnyServer package is now published to NuGet as well, which fixes the previously-broken version of the DafnyLanguageServer package. (#2787)
• fix: Support for spaces in the path to Z3 (#2812)
• deprecate: Statement-level refinement syntax (e.g. assert ...) is deprecated (#2756)
• deprecate: The form of the modify statement with a block statement is deprecated
• docs: The user documentation at https://dafny.org has a new landing page