[Arnavion]

Rust won't help. Sure the compiled code would be bounds-checked, but nobody would notice the bug unless they gave it the crashing input. And then when they reimplemented the code in their non-bounds-checked language then that would reintroduce the bug anyway.

A formal verification implementation would catch it at authoring time, yes.

[ysleepy]

It seems to be an array out of bounds read/write. Rust does bound checks, so this should be covered.

[GoblinSlayer]

All languages except for C do bound checks, you don't need a borrow checker for this.