We want to develop a standard library of differential operators that can be used to program complex incremental computations. A differential operator maps changes of its input to changes of its output while exploiting algebraic properties of the underlying non-incremental operation to avoid unnecessary work. We present a general framework for developing and verifying such differential operators. We formulate this framework in Coq and have successfully verified several existing efficient differential operators and used it to develop new ones.