[nickbauman]

Not saying you're wrong: At the end of the day to the degree that any of these methods (UML, TLA+, whatever) formally prove correctness is the same degree that they gain the features of a turing-complete programming language. Which comes back to the notion design is the source code itself and represents the majority of the work. The compiler or interpreter is the "construction" phase of the project.