[ip26]

It's a complementary tool that replaces certain difficult types of testing. Viewed this way, you can focus writing formal specification for things which are easy & clear to formally specify. "this returns sorted lists" is, for example, a simple property. Other examples might be the O(n) performance of your algorithm. Meanwhile, "every input can be found in the output" might feel too painful to write, so you might compromise on "the output has the same number of elements as the input". This leaves plenty of space for classical testing, while unburdening classical testing from worrying about select classes of bugs.

One other valuable part of formal methods is forcing the author to make claims about their program, and then poking holes in those claims. This process helps the author understand their own code better, and after a process of iteration developing the formal properties that are actually true, you now have a strictly-true external interface specification for the program. This is obviously most-valuable for only certain classes of code, such as libraries or services.