That is not true at all. You do not need to generate a spec. All you need to do is prove a property. This can be done in many ways.

For example, many things can be proven about the following program without having to solve any general problem at all:

echo “hello world”

Similarly for quick sort, merge sort, and all sort of things. The degree of formality doesn’t have to go to formal methods which are only a very small part of the whole field