Leslie Lamport: Video course on TLA+
Great to see this here! I act as a TA for Dr. Lamport&#x27;s TLA+ courses at Microsoft, and can answer any questions y&#x27;all have.<p>TLA+ in one sentence: it is a language used to write specifications, same as you might write a spec in English&#x2F;your chosen informal language, except here you write your spec in basic mathematics; benefits of a formal specification language include freedom from ambiguity, model-checking, and even machine-checked proofs of correctness.<p>This language is a joy to use and I&#x27;ve found it really affects the way I think about system design.