It's a continuum... but I would say even Rust's type system is not in the realms of "formal verification". I think you need at least some kind of refinement types so you can say "an integer between 1 and 10" before you can stake even a vague claim to "formal verification".

So I don't think you can say it's common in the software world.

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.