When developing fully verified implementations, mutable state is often necessary to achieve good performance, as it underlies important optimisations, but has a substantial verification cost: one must either commit to a deep embedding or follow a monadic style of programming. An alternative is to use what we call adjustable state. We extend Coq with a type of adjustable references, which are like ML references, except that the stored values are only partially observable and updatable only to values that are observationally indistinguishable from the old ones.