Specifying that a value must be an integer between 1 and 10 is most certainly further down the continuum than only specifying that a value must be an integer, but both define a theorem about the program that can be validated. How is the latter not formal verification? It's the same thing, only differing by degree.