Thanks! Good question, I don't think such a tool exists. Such a tool would require a mathematical proof of an invariant that all the accesses are in bounds. The closest thing is the compiler's own bounds-check elimination proof engine. It eliminates the check when it can prove the checks aren't necessary and sometimes you can help it with hints like `_ = b[i+3]`. But then you don't need unsafe at all, which is the point: unsafe is the last resort.