State Machines are the natural paradigm in TLA+. OOP is just poorly organized state machines. Try rewriting an OO program with state machines and you’ll have so

State Machines are the natural paradigm in TLA+. OOP is just poorly organized state machines. Try rewriting an OO program with state machines and you’ll have something that directly maps to TLA+, and it should demystify much of formal verification.