A ppx reduces a bit the pain (see tensority/examples/ma.ml at master · Octachron/tensority · GitHub for instance), but it does not really alleviate the core issue that the OCaml type system is not great for proving arithmetic properties.
My current opinion is that the best compromise might be to use a core module and phantom types to encode the smallest set of property that you want to check. For instance, src/Indexing.mli · master · POTTIER Francois / fix · GitLab defines an iteri function where the type system reflects that the index provided by iteri is always safe to use to access elements of vector of the same semi-static size:
val iteri : ('size index -> 'elt -> unit) -> ('size, 'elt) vector -> unit