What you are looking for are refinement type systems. LiquidHaskell [0] is the most well known refinement type system out there, to specify and verify these kind of assertions.

[0]: https://ucsd-progsys.github.io/liquidhaskell-blog/