Loop invariant condition IsPrime program
The condition $2 \leq i \leq \lfloor \sqrt{n} \rfloor$ is a reasonable part of the invariant you seek. As I think you realize, this is not enough.

You proposed to also require $n \!\!\!\mod i \neq 0 \implies n$ prime, but this can not realistically hold. For instance, take $n=3^2=9$: running the loop we would start from $i=2$ and have $n \!\!\!\mod i = 1 \neq 0$ but clearly $n=9$ is not prime, which makes the condition false. Hence, that is not really an invariant.

What we need is something expressing "we checked all the numbers from $2$ to $i-1$, and we did not find any divisors". This can be written as "for all the numbers $k$ such that $2\leq k &lt; i$, we have $k\!\! \mod n \neq 0$".

That might be enough, but the loop seems to have a bug to me: for e.g. $n=5^2$ we never try to divide for $i=5$, consequently returning that $25$ is prime. Perhaps you should fix the bug first, and then adapt the first "range" invariant accordingly.