From what I've seen, those are poorly done in practice, usually in multiple ways.

Recently I've been writing code to deal with partial alignment. The desired invariants here typically involves at least 3 variables:

  align must be a power of 2. Since this involves only one variable, refinement types can handle this one just fine at least (expression: n && !(n & (n-1)) ).
  0 <= skew < align
    skew != 0 in some branches, additionally
  pointer_as_int(buf.start) % align == skew
    some APIs take 2 buffers that should both have the alignment
    often if the buffer points to a size-zero span at NULL, the condition does not need to hold however
  (skew + buf.len) % align == 0 (only relevant sometimes; sometimes this is a different alignment than other invariants)

Since these are, generally, separate function arguments with completely different origins, how do you apply refinement types here? Additionally, the buffer can have different kinds of external ownership; in particular, Rust's aggressive "I must move ownership without warning" makes it impossible to write a lot of good code. We must not abandon the good parts of C if you want people to actually use your stuff, even ignoring the incremental-conversion problem.

Now consider ABI compatibility, say if we had forgotten to add the skew != 0 condition somewhere. If old code calls the function, it needs to hit a thunk that verifies the condition. New code however should have done that in the caller and thus enter the code directly. Where is the compiler tooling to support this? Clearly, invariants (and pre- and post-conditions, which are just invariants for a finite time) need to be able to specify what version of your code they were first specified in. That's a lot of information to specify in a function type which often gets disregarded.