Interconnect delay in the routed circuit becomes dominant as process technology goes into deep submicron range. Buffer insertion is one of the most effective techniques to reduce the interconnect delay. However, when multiple operation modes and process corners are taken into consideration, the number of possible solutions of existing works grows exponentially. In this work, we present a 3-phase buffer insertion and sizing technique taking the advantage of formal engine while the multi-corner multi-mode (MCMM) timing constraints are satisfied at the same time. The experimental results show that our approach can achieve 62.14% buffer area reduction on the most critical path on average within a reasonable runtime.