So say you were writing a sorting algorithm and with unit tests (perhaps with TDD) you wrote tests like:
- sort([]) should produce []
- sort([1]) should produce [1]
- sort([1,3,2]) should produce [1,2,3]
- sort([1,5,6,2,3,4]) should produce [1,2,3,4,5,6]
You would test a few values and edge cases until you were confident it works for all lists. However, you can't be 100% sure that there's some list out there like [5,5,5,5,1] that doesn't get sorted properly.
With formal verification, you can actually test it sorts for all possible lists with a mathematical proof. You write a maths proof that shows a property like the following holds:
- For all lists X, the result of sort(X) will be a permutation of X that is sorted.
For example, the proof could take the form of proof by induction where every step in the proof is confirmed correct by the machine (see Coq, Isabelle for more info).
When you were doing maths at school, you probably had exercises where you tried a few examples to see if an equation you came up with might hold in general and then you would write a proof to showed it worked for all possible cases (e.g. with induction, by case analysis). The former is similar to unit testing and the latter is similar to formal verification.
My point was there's a spectrum of how rigorous your tests are. People talk about TDD like it's the holy grail sometimes but it's nowhere close to how rigorous you can be. If you've tried some formal verification though, you'll realise it's far too expensive for most projects. Likewise, TDD doesn't make sense for all projects.
You have to pick your tradeoffs e.g. between time to market vs cost vs ease of refactoring later vs how rigorous the testing is.