  We present a simple and concise semantics for temporal planning. Our
semantics are developed and formalised in the logic of the interactive theorem
prover Isabelle/HOL. We derive from those semantics a validation algorithm for
temporal planning and show, using a formal proof in Isabelle/HOL, that this
validation algorithm implements our semantics. We experimentally evaluate our
verified validation algorithm and show that it is practical.
