My formal proofs for C or C++ take almost no time to write at all, because I'm using the right tools. Some asserts, some _CPROVE_assume hints, and mostly limitation of big for loops or recursions. If it works for 6, it also should work for 1000.