Thorough automatic testing is valued by agile practitioners because it lets them move faster even thought it might initially seem like more testing means more w

Thorough automatic testing is valued by agile practitioners because it lets them move faster even thought it might initially seem like more testing means more work means slower iterations. I think a similar effect is possible when you use specification languages and model checkers as part of an agile way of working. The spec is at a higher level than the implementation and hopefully radically shorter and easier to adapt. The model checker then lets you find flaws in design changes faster than you would have without it.