I am the guy assigned to work on that: sorry for the delay, but it is being worked on.
there are also the z3-integration related checks which might even apply to index bounds or eventually other invariants, so this kind of safety is important for Araq and Nim https://nim-lang.org/docs/drnim.html