New features

• Added opaque blocks to the language. Opaque blocks enable improving verification performance. See the documentation for more details. (https://github.com/dafny-lang/dafny/pull/5761)

• By blocks (... by { ... }) are now available for assert statements, call statements, and the three types of assignments (:=, :-, :|). Also, by blocks should now be more intuitive since they enable proving any assertions on the left-hand side of the 'by', not just the 'outermost' one. For example, previously assert 3 / x == 1 by { assume x == 3; } used to give a possible division by zero error, but now it won't. (https://github.com/dafny-lang/dafny/pull/5779)

• Use --suggest-proof-refactoring to be alerted of function definitions, which have no contribution to a method's proof, and facts, which are only used once in a proof. (https://github.com/dafny-lang/dafny/pull/5812)

• Support for top-level @-attributes (https://github.com/dafny-lang/dafny/pull/5825)