This could should be able to go without a bounds check. i cannot be negative at the beginning. In order to become negative, it must overflow. However, it cannot overflow: It is being incremented, so it must reach len(a) before overflowing, in which case we exit the loop before evaluating a[i].
(I actually know a priori in my code that i is not negative; I'd be tempted to use #30582 here. I could also switch to i being a uint, which does remove the bounds check, but it makes other things in the real code a bit awkward.)
I don't know how hard it is to teach prove about this case.