> TLA+ is not panacea Of course it isn't, but neither is testing, and we all still do it. The only question that matters is, does it have a good ROI or not? TL

> TLA+ is not panacea Of course it isn't, but neither is testing, and we all still do it. The only question that matters is, does it have a good ROI or not? TLA+ does in a wide range of problems. > which means its users will still need to master temporal logic, first-order predicate logic, formal specification, and a slew of concept That all sounds imposing, but TLA+ users usually don't "master" any of those, and reaching a level of high utility takes far less time than achieving the same with any programming language. Writing useful specifications that can save real money takes something like 3-4 full days of a workshop or 2-4 weeks of after-hours self study. Learning how to read specifications well enough to implement them takes much less (a few hours to one day), and doesn't require any temporal logic at all. It's certainly possible that it's still not for the majority of engineers, but most teams will have at least one person who can do it, and that might be enough. > such as spurious counterexamples ???