This paper describes a formal repair framework for performance bugs in loop programs, which are programming errors that slow down program execution. The approach is developed based on the observation that a program with a performance bug is a semantically correct program, but it may perform inefficiently for some inputs. This observation permits the formal treatment of performance bugs using the idea of program invariants, where the original program is augmented with a number of non-functional variables that are used to assess the efficiency of the patched version vs. the original program using the derived invariants. The proposed approach offers two major advantages compared to the conventional test-based patch validation approach. First, it enables the formal validation of patches using program verifiers. Second, it helps to assess the efficiency boost provided by the generated patches. To the best of our knowledge, the formal treatment of performance bugs has not been studied in the prior literature.