Automated program repair (APR) techniques that use test suites for bug localization and assessing candidate patches have promising results. Studies have shown that generated patches by APR tools that pass its test suite do not always correctly implement the program’s expected behavior, known as test overfitting. My research aims to provide fresh insight into the test overfitting problem by using formal methods.