[Y_Y]

> TLA+ is a formal specification language developed to design, model, document, and verify concurrent systems.

[kaba0]

But it only proves a model, not the actual code — that’s a major distinction.