Weakest preconditions are essential notions for program verification. There are many variations of weakest preconditions, and their uniform treatment has been studied using category-theoretic notions like monads. In this talk, we consider weakest preconditions for a higher-order functional language with computational effects and recursion and show that we can syntactically compute them via a CPS transformation. We prove our main theorem in a general setting, which enables us to instantiate our result to several problems of program verification. Our result generalises two existing works on program verification: (1) trace properties and may-/must-reachability studied by Kobayashi et al.\ and (2) expected cost analyses studied by Avanzini et al. We also obtain a new instance of cost moment analyses using our main theorem.