strlen proven, but not by me

size_t strlen(const char *s)
{
	const char *sc;
	/*@ loop invariant s <= sc <= s + strlen(s);
	    loop invariant valid_str(sc);
	    loop invariant strlen(s) == strlen(sc) + (sc - s);
	    loop assigns sc;
	    loop variant strlen(s) - (sc - s);
	 */
	for (sc = s; *sc != '\0'; ++sc)
		/* nothing */;
	return sc - s;
}

Where is the /*@ comment for this function? We’ll come to that in a minute ...

Proof by Denis Efremov, Ivannikov Institute for System Programming at the Russian Academy of Sciences, https://github.com/evdenis/verker/blob/master/src/strlen.c