> And is that model common across other proof systems like TLA? Yes, it's pretty common, and is a really nice abstraction. TLA+ doesn't use that model, althou

> And is that model common across other proof systems like TLA? Yes, it's pretty common, and is a really nice abstraction. TLA+ doesn't use that model, although a lot of TLA+ code is implemented that way. TLA+'s model is basically "shared memory" where any step can access or change any state in any way it likes. That's super flexible, but can feel a little too flexible. P, on the other hand, is based on a model of state machines that communicate with messages. See this example for a clear illustration of how that works: https://p-org.github.io/P/tutorial/twophasecommit/ https://p-org.github.io/P/tutorial/twophasecommit/