> In the TLA+ formulation, and we can think of an adversary as an agent in the system who can take a superset of the actions everybody else can.

Sounds a lot like a Dolev-Yao adversary, which is used in protocol verification tools like Tamarin.