We present an automated approach to repair programs using formal verification and expression templates. In our approach, an input program is first verified against its formal specification to discover potentially buggy statements. For each of these statements, we identify the expression that needs to be repaired and set up a template patch which is a linear expression composed of the program’s variables and unknown coefficients. Then, we analyze the template-patched program against its specification to collect a set of constraints of the template patch. This constraint set will be solved by a constraint solving technique using Farkas’ lemma to identify the unknown coefficients, consequently discovering the patch. We implement our approach in a tool called Maple and evaluate it with various buggy programs from a widely used benchmark TCAS as well as a synthetic, yet challenging benchmark containing recursive programs. Our tool outperforms state-of-the-art program repair tools in returning desired patches.