Delimited continuations are used in algebraic effect handlers and shift/reset contructs. Both language features allow monadic coding style to be naturally supported by imperative programming languages. Our attempt at reasoning with effect handlers in 2023, had led us to design a new logic, called staged logic, that is capable of handling both effectful higher-order programs and delimited continuations. We have recently also extended staged Hoare logic to support specification and verification of imperative programs with Danvy and Filinski’s shift/reset constructs.