TL;DR
ループの実行前にも、反復するたびにも成立する条件。
不変条件の一種である。
仕組み
Wikipedia によると、ループ不変条件はループの意味を理解するうえで重要で、コードの中にアサーションとして書かれることもある。プログラムの正しさを示すときは、ループに入る前に条件が成り立つこと（初期化）、各反復のあとも成り立ち続けること（維持）を確かめる。ループが終わった時点では、不変条件とループの終了条件の両方が成り立つ。
ホーア論理などの形式検証では、ループ不変条件を述語論理の式で表し、アルゴリズムの正しさを証明する。
例
Wikipedia では、配列 a の最大値を求める関数を例にしている。ループの中では「m は a[0...i-1] の最大値である」が不変条件になる。ループが終わると、不変条件と i == n の両方が成り立つので、m は配列全体の最大値になる。