[pierrefermat1]

I've only play with TLA+ for a small amount of time but absolutely agree with the maths statement being way off the mark.

Building out any real maths with logic operators yourself is just not feasible in a meaningful timescale.