Dafny is incredibly powerful. With it, you can prove type safety properties of a programming language, you can verify runtime complexity of an algorithm, you can identify conflicting specifications, and much more. In many cases, verification provides all the correctness guarantees that you need for your project. However, if you want to integrate Dafny code with existing codebases, you may face challenges that verification alone might not solve and where runtime testing could be useful:
