TLA Plus

#tlaplus

I just read an incredible paper written by engineers at AWS: Use of Formal Methods at Amazon Web Services

I find complex distributed systems fascinating. Reading about the use of mathematics to verify the correctness of distributed systems was very eye-opening.

Some highlights from the paper:

So far we have used TLA+ on 10 large complex real-world systems. In every case, TLA+ has added significant value, either finding subtle bugs that we are sure we would not have found by other means, or giving us enough understanding and confidence to make aggressive performance optimizations without sacrificing correctness.

This was a very subtle bug; the shortest error trace exhibiting the bug contained 35 high-level steps.

That spec did not uncover any bugs but did uncover several important ambiguities in the documentation for the algorithm, which the spec helped to resolve

I would also recommend checking out The TLA Home Page

Hands-on debugging session: instrument, monitor, and fix

Join Lazar for a hands-on session where you’ll build it, break it, debug it, and fix it. You’ll set up Sentry, track errors, use Session Replay and Tracing, and leverage some good ol’ AI to find and fix issues fast.

RSVP here →