We present a deductive synthesis procedure that generates runner implementations from coinductively defined specifications of behaviors exposed by the environment and those expected by the client. Our procedure can then be used as a correct-by-construction technique to synthesize runners which can be used to mediate between effectful clients and stateful environments that provide interpretation for the effects. We further demonstrate that copattern-based terms possess a close connection to actual runner implementations expressed as top-level handlers in OCaml, thus providing a practical correct-by-construction synthesis procedure. We intend to present this talk for 30 minutes, and provide an overview of our synthesis procedure and real-world applications such as logging, scheduling, process communication, and state management.