This work proposes a novel approach for automatic verification and synthesis of infinite-state reactive programs with respect to \(CTL^*\) specifications, based on translation to Existential Horn Clauses (EHCs). \(CTL^*\) is a powerful temporal logic, which subsumes the temporal logics LTL and CTL, both widely used in specification, verification, and synthesis of complex systems. EHCs with its solver E-HSF, is an extension of Constrained Horn Clauses, which includes existential quantification as well as the power of handling well-foundedness. We develop the translation system \({\textsf {Trans}} \) , which given a verification problem consisting of a program P and a specification \(\phi \) , builds a set of EHCs which is satisfiable iff P satisfies \(\phi \) . We also develop a synthesis algorithm that given a program with holes in conditions and assignments, fills the holes so that the synthesized program satisfies the given \(CTL^*\) specification. We prove that our verification and synthesis algorithms are both sound and relative complete. Finally, we present case studies to demonstrate the applicability of our algorithms for \(CTL^*\) verification and synthesis.