First, generalized static invariants that are either correct all the time or computable all the time are, impossible, of course. Even of the simple form you are trying. Second, Ada 2012 has static type invariants (enforced at compile time) and dynamic type invariants (enforced at runtime)

You should be able to do, at the very least, what you are doing, in a much simpler way.

Plus, it has procedure level pre and post conditions that are checked

In any case, the tools ADA has allows it to go further than what you want, actually. https://en.wikipedia.org/wiki/SPARK_(programming_language)

There is a formally verifiable language that is just a subset of ada (IE compilable as normal ada) but can formally verify what you want here even if static predicates can't.

(Now all of the above said, i'm not sure i'd go this route, but yeah)