> The biggest pitfall wrt. TLA+ is that it's not intended as an end-to-end system. That's a huge benefit, rather than a pitfall at all. End-to-end verification

> The biggest pitfall wrt. TLA+ is that it's not intended as an end-to-end system. That's a huge benefit, rather than a pitfall at all. End-to-end verification of real-world systems ranges between the impractical through the infeasible to the downright impossible. The biggest software ever verified end-to-end at the same depth as TLA+ was 5x smaller than jQuery, required extraordinary simplification, and still took world experts years. People have found serious bugs in software ten times the size of the largest program even verified end-to-end within days of starting to learn TLA+. The question is not whether TLA+ can achieve a feat nothing else can, anyway, but whether it has a good ROI.