Refactoring legacy code seems like something where formal methods could help. "Prove that these 2 subroutines are equivalent, across all inputs" is exactly the kind of thing that they're good at!