> failure but TLA+ proved that it was impossible to build a reliable system based on the hard requirements
That's probably the most useful result TLA+ can give in comparison to not using it.
Understanding that requirements are impossible after 1-2 weeks of modelling is way better that after 6+ months of coding.