Their corrected version:

    if (n > 0 && runLen[n-1] <= runLen[n] + runLen[n+1]  
    || n-1 > 0 && runLen[n-2] <= runLen[n] + runLen[n-1])

In the first clause they add earlier to later runLen elements, but in the second they add later to earlier elements. Switching the order just makes the expression harder to understand, like reusing variables within a scope. Addition is commutative and there's nothing technically wrong with it, but this construction makes it appear like there may be something special about element n when there's not.

The programmer also has to do mental arithmetic to check the bounds. Bounds checks can be written so that the largest index subtracted is also the value tested:

    if (n >= 1 && runLen[n-1] <= runLen[n] + runLen[n+1]  
     || n >= 2 && runLen[n-2] <= runLen[n-1] + runLen[n])

This makes it easier to see that the bounds are correct. Formal methods found an important bug that would not have been found otherwise, but a lot of lesser bugs can be prevented just by writing clear and consistent code.