As I will discuss in part 4, the algebraic approach most similar to TLA is Ralph-Johan Back's and Joakim von Wright's refinement calculus/algebra. However, AFAIK, it doesn't (yet?) handle concurrent algorithms, whereas in TLA concurrent and sequential algorithms are formally indistinguishable (they are only distinguishable by how a reader informally interprets the formula; see the mention of "processes are in the eye of the beholder" in the post).