Abstract: Software testing can find errors, but can not find them absent. Because program verification can provide this guarantee, it has arguably been one of the most fertile application areas of formal methods and becomes more and more important in software development. Proving the correctness of a program entails showing that if the program is initiated from a machine state satisfying a certain precondition then the state on termination satisfies some desired post-condition. The emphasis was put on formal verification in program proving previous. If we can algebraize program proving, the correctness proving can be mechanized and automated easily and the efficiency of proving can be also improved greatly. Wu’s method has been shown to improve efficiencies in mechanical geometry theorem proving, where it can replace the well-known Grobner basis method. It seems to have promise to bring the powerful mathematical machinery to settle the program total correctness problem. This study applies Wu’s characteristic set method and mathematical induction to proving the total correctness of recursive program. Our method is based on the algebraic theory of polynomial set, which have wider application domain. We implement this method with the computer algebra tools MMP. The application of the method is demonstrated on a few examples. Compared with proving tool Isabelle, our method is more efficient through experiments and greatly improves the efficiency of proving especially in polynomial program. In this way, an algebraic approach based on mathematics mechanization is introduced to software verification. A new idea for program correctness proving is proposed in this study.