If TLA+ is hard to adopt because formal methods are inaccessible for most programmers I guess this can be avoided if we had progressive self assessment tools, where we can exercise our understanding the further we progress.

I am not aware the existence of such tools, for TLA+ and since I didn't find any, I have decided to build one But I want to check with you if this approach is relevant.

If a tool exists please cite it to me, If not, I'd love to share with you my approach in another post which is based on Computer Adaptive Testing, and item response theory,

Looking forward to hear back from you