>Automated tests are a formal specification, and running them is a formal verification method. This is a great way to describe it, and an important concept to

>Automated tests are a formal specification, and running them is a formal verification method. This is a great way to describe it, and an important concept to grasp. Another kind of formal verification that exists between "standard" unit tests and model checking/automated theorem proving is property-based testing a la quickcheck: You have a function you want to test (e.g., a sort), you describe the properties of inputs ("a list of integers") and state the properties you want to hold of the output ("every number should appear the same number of times in the output as in the input, and every number should be >= the number to its left") and ask the system to generate and test lots of random inputs for you. These properties can often be used more or less directly in model checkers, which makes the checking exhaustive (on some small, finite domain).