With --standard-libraries you can now read an 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. (ht tps://github.com/dafny-lang/dafny/pull/6286)