DTest is an automated test generation toolkit for the Dafny programming language. You can run DTest on your Dafny code and it will automatically produce tests that guarantee statement or path coverage (depending on the settings). Under the hood, DTest relies on the Dafny verifier to generate test inputs that reach the requested section of your code. You can also use DTest as a linter to uncover dead code.

GitHub Repo: https://github.com/dafny-lang/dafny (DTest is officially part of Dafny)

Paper (NFM): www.amazon.science/publications/a-toolkit-for-automated-testing-of-dafny

If you want to learn more about DTest, read the official Dafny blog.