TLA+
TLA+ (Temporal Logic of Actions) is Leslie Lamport’s “formal specification language … for designing, modelling, documentation, and verification of programs, especially concurrent … and distributed systems.” It’s the specification + model-checking wing of formal methods, distinct from the theorem-proving wing this wiki already has (lean-theorem-prover, alphaproof). Source: Wikipedia.
How it differs from a proof assistant
Where Lean/Coq prove mathematical theorems interactively, TLA+ specifies system behavior and checks it by finite model checking (TLC): it “finds all possible system behaviours up to some number of execution steps, and examines them for violations of … safety and liveness.” Set theory for safety (“bad things won’t happen”) + temporal logic for liveness (“good things eventually happen”). (TLAPS adds machine-checked proofs, but model-checking is the core.)
Why it matters here
Industrial design-bug finding before implementation: AWS used TLA+ to uncover bugs in “DynamoDB, S3, EBS, and an internal distributed lock manager; some … required state traces of 35 steps,” and Microsoft uses it for Cosmos DB. It broadens the wiki’s formal-methods cluster from proving math (Lean/AlphaProof) to verifying systems — the same “mechanize rigor” impulse aimed at engineering rather than mathematics, a closer cousin to everyday software than the proof assistants.
Related
lean-theorem-prover · alphaproof · lean-for-programmers · tools-for-thought