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)

Ada does a mix of both compile-time and run-time checks. It was systematically designed to eliminate errors in most parts of the development process as the book below shows. SPARK, an Ada variant, can prove absence of all kinds of errors in code with automated provers. Since Ada supports cross-language programming, the typical route is to do most of the key logic in Ada, anything static/simple in SPARK, and anything platform-related in native language if too hard to do in Ada. They periodically update them with recent versions at 2012 for Ada and 2014 for SPARK.

http://www.adacore.com/uploads_gems/Ada_Safe_and_Secure_Book...

Note: See table of contents especially.

http://cowlark.com/2014-04-27-ada/index.html

Note: This "random walk through Ada" has a nice summary of all kinds of features it has from perspective of an outsider instead of an Ada developer.

https://en.wikipedia.org/wiki/SPARK_(programming_language)

http://www.adacore.com/uploads/technical-papers/SPARKSkein_S...

Note: Link to SPARK and an example by Rod Chapman on doing Skein in it. Just converting it from C to SPARK found an error in original code. Because of course it did haha...

Idris or F*? I think they are not practical because compile times end up extremely slow. I think want you want will necessarily have this effect of very slow compile times.

Came here to suggest Idris, as it compiles to C. F* is still experimental and Idris is just coming up on a RC. They could also drop down into C and manually verify it.