> Every government IT project that is years late and billions over budget is because of this

Well, that used to seem to be true before governments started experimenting with (methodologies which were notionally versions of) Agile, Lean, and related ideas. Then there were a whole new set of reasons for IT projects being years late and over budget.

False. Writing a waterfall-style “spec” on paper has nothing to do with formal methods.

It absolutely does. We studied SSADM in college.