Arguably, if 'real' Agile is ever found Formal Methods would be the antithesis of it: something provable and reproducible is blasphemy to True Believers.
Not at all. Something that you can't easily change is terrifying.
Reproducible? Sure, that's what unit tests are for. Make a change, prove that you didn't break any behavior that anybody relied on.
But if you have to do a three-month-long formal proof run because the specification had a one-line change, then you're not agile, under any meaningful definition.
(Where did three months come from? Thin air. I don't know how long a true formal proof would take. Depends on how many things you're proving, how long your spec is, and how much CPU power you have. I would think, though, to formally prove significant properties of a large code base would take a significant time.)
