I believe I've read about some languages with invariant using them at compile time to verify the value meets the invariant, if possible. For example, let's say a function's invariant guarantees it returns an even integer, and then we pass that into a function that only accepts odd negative integers, it could catch that during compile time. To me, that's the coolest case for invariants.

Again, I believe that this is a PL research topic, but I'm not super well versed in it, so take that with a grain of salt.