It's a set of asserts that are a part of the type signature. Requires are asserts on the inputs, ensures are asserts on the outputs.

Depending on your backend you either ignore them, check them all of the time, some of the time, or have SMT-solvers prove that if you uphold the first one all else must follow.

If you're interested in the last one, have a look at Dafny[0]

[0] https://dafny.org/