Common engineering practices today use testing to ensure the quality of software. But relying solely on testing has several well-known drawbacks, such as only testing the program for the given inputs and applying tests only after the entire program has been developed. An idealistic, long-standing dream has been to formally verify the correctness of program, for all inputs. Is there some reality in that dream?

In this talk, I present Dafny, a state-of-the-art tool for program verification. Dafny has been used to verify the full correctness of some challenging algorithms. It was used by two medalist teams in the VSTTE 2012 program verification competition and is being used in teaching. Through demos of this research prototype, I show the vision for how a program verifier can help during software development.