Formal verification is a stricter way of ensuring correctness of a program, but sitting down
and writing the proof yourself is often time-consuming. SMT solvers try to automate parts of this
process. This paper aims to explore Dafny, a programming language and verifier that uses an SMT
solver underneath to do this verification. This paper will go over its logical foundations, and how
it can be used to verify an in-place selection sort algorithm as well as a key-value store. It will
also explore a feature of Dafny that allows the user to compile to other languages, and will discuss
its usefulness in the industry. Verifying the sorting algorithm was very straightforward while the
key-value store posed some problems. However, Dafny itself seems to be very straightforward
to program in. Its ability to compile to other languages leaves a lot to be desired. While the
compiled code is fully functional, the code is barely readable and less than ideal to work with. A
further study discussing Dafny’s ease of use compared to other tools could be conducted to see if
the lacking compiler could outweigh having a native verifier specifically designed for a high-level
programming language.