dafny-lang/dafny v4.9.0 on GitHub

New features

Added opaque blocks to the language. Opaque blocks enable improving verification performance. See the documentation for more details. (#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. (#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. (#5812)
Support for top-level @-attributes (#5825)

Enable abstract imports to work well with match expression that occur in specifications (#5808)
Fix a bug that prevented using reveal statement expressions in the body of a constant. (#5823)
Improve performance of dafny verify for large applications, by removing memory leaks (#5827)
Green gutter icons cover constants without RHS (#5841)