If your tests cover all branches of a loop, then it doesn't matter if a loop invariant is violated within the loop. Write tests that exercise the {0, 1, Some, Bounds} branches, verify that the result is correct. Then go on with your life knowing that there's no possible way that the code breaks without either failing the tests or changing the branch coverage.

Put another way (and taking the max() implementation from the wikipedia article. If I implement the max function in a way where in the first loop iteration I add 1 and in the last I subtract 1, then the loop invariant doesn't hold but the result is correct. The assertion approach fails, but the test approach succeeds because I have tests for {0, 1, Some} iterations.

: It would be silly to do this, but I'm trying to present a minimal counter-point here. You could extrapolate this type of change to a change made for performance purposes which are less obviously correct, and which may cause this type of internal invariant to be false. The argument is the same.

An assertion can tell you if one of your assumptions is incorrect.

Combined with fuzz testing, you can have much higher confidence that your code is correct.

This is a stronger guarantee of program correctness than any set of unit tests you're likely to write.