My point was that that may not be the actual invariant. By making your invariants explicit these tools have a better chance of finding real errors since you compare the code against a specification. Deriving a specification just means your code works according to itself.