[eyelidlessness]

Define a model of your program’s state, as if you’d define a model in a database. There, that’s your program! It is actually a database. You can’t create invariants in the program. It’s entirely defined by how you modeled it. Your program is correct.