I can't say I fully understand what you're saying (you use some uncommon terminology without defining it), but expressing algorithms mathematically does not imp

I can't say I fully understand what you're saying (you use some uncommon terminology without defining it), but expressing algorithms mathematically does not impose any style or order on the exploration of the problem. It just gives you a language that is far more flexible for talking about both your problem and your solution at any level of detail that you choose than any programming language. TLA+ certainly allows you to describe a system as a set of scenarios/properties (what I assume you would call tests), and also of asserting that a design satisfies them. There was a system I worked on that was so complex that I was only able to design it using TLA+; engineers at Amazon, Microsoft, Oracle and Intel report similar experiences.