Another possibility that doesn't require such heavy language machinery is something like OCaml's private types, where the scope of unrestricted access is unsafe blocks rather than the body of a module. In this approach there is no type-level correspondence between the value of the length member and the extent of the array: private types only ensure that any potentially invariant-breaking mutation is restricted to a certain scope, not that the code is correct.

Object invariants are assertions which must be true whenever control is not within the object. The object invariants must be true when control leaves the object by exiting any public function. Nothing outside the object must be able to alter the variables involved in the object invariant. Only one execution thread can be in the object at a time. If you can demonstrate all of those conditions, assuming the invariant is true at entry to the object, you have proved the object invariant.

This is a useful and well-understood concept in the proof world, but isn't seen much in programming languages.