I agree with you about the potential value of formal methods, but I think you completely missed the point of the article. Formal methods can't supply specifications. They can perhaps tell you if your specification is consistent and therefore implementable, but they can't tell you whether the system you've specified will meet your needs.

I think those of us who promote formal methods need to remember this. At best only verification -- making sure the implementation matches the specification -- will ever be fully automated. Validation -- making sure that what we specified is actually what we wanted -- will always be a human activity.