In this talk we discuss our work on techniques to aid the verification of programs whose state evolves monotonically according to a preorder (a reflexive, transitive relation). We give a formal account of a useful verification model: a property witnessed at some state s0 can be safely recalled at any future state s1, so long as the state evolves monotonically and that property is stable with respect to the given preorder. Specifically, we study this style of verification in the context of the effectful dependently typed programming language F*. While specific instances of this verification model are used extensively in F*, their use has been somewhat ad hoc so far. In this work we provide a general framework for this style of verification: we develop a preorder-respecting version of F*’s state effect, equip it with an instrumented operational semantics, and demonstrate how the instances of this verification model already used in F* can be implemented in our general framework.