Extracts a TLA+ specification from concurrent or distributed code, modeling the state machine, actions, and fairness conditions for model checking with TLC. Use when verifying concurrency properties of production code, when designing a protocol and wanting to check it before implementation, or when the user has a race condition and needs to prove the fix.