It can actually be used in a variety of ways. It can be a runtime assertion. It can also be used to automatically generated unlimited tests (using property-based testing, similarly to Haskell and other languages) and that can be done at compile time. That is, you write a spec for a function and the tests are automatically created to ensure that all valid input the function can handle matches corresponding output it emits.

Because these are not actual static types, you can get a lot of control and say things like "this function accepts three arguments, all integers between 5 and 50, but in increasing order, and the output must be a float between 0 and 1", and then have that checked on the function before the program ever runs. At run time, you can then verify that you are passing in valid arguments.

Spec is relatively new, and there are experiments in the community to do things more like traditional static type checking also. The future is an interesting place.