Hey I found this implementation on a codeforces blog. What do you think about it , is this the most easy and reliable implementation according to you (for solving the problems)? I am asking because there's so much confusing stuff about loop invariants and I just want something which always works for sure!

l, r = -1, n
while r-l > 1:
    m = (l+r)//2
    if F(a[m]):
        l = m
    else:
        r = m

You can easily prove that l = k and r = k + 1 by the end of the while loop. In this case no worries about whether to increase m by 1 or not.