This stuff has been out there for a long time, but it's never become popular outside of outside of safety-critical or high-integrity systems. Examples include:

Microsoft's C/C++ annotations: https://docs.microsoft.com/en-us/visualstudio/code-quality/u...

Ada's ranges: https://en.wikibooks.org/wiki/Ada_Programming/Types/range

Fun stuff to learn about in theory, but, unless you're working at a place where formal verification is part of the culture, good luck selling these tools to upper management.

More resources discussed here: http://highscalability.com/blog/2018/9/19/how-do-you-explain...