tlaplus-systems-engineer

Identify actors, shared state, environment actions, and safety invariants, then write TypeOK, Init, named sub-actions, and Next composed from them. Start with the smallest useful model, such as two agents and a bounded queue, and run TLC before adding liveness.

Use PlusCal for algorithmic workflows with loops, retries, and process-local control flow, since it generates pc states automatically. Use raw TLA+ for declarative protocols, relation-heavy state, or highly abstract specifications not tied to program-like control flow.

Use TLC for finite explicit-state bug hunting and invariant checking, and TLC simulation when the space is too large for exhaustive search. Use Apalache for bounded symbolic checking of arithmetic-heavy models, and TLAPS when properties must be proved beyond any finite instance.

Shrink constants and domains, replace payloads with symbolic tags, use sets instead of sequences when order is irrelevant, and split oversized actions with a program counter. Add symmetry or state constraints only after the model itself is clean, then consider simulation or Apalache.

Yes. Model the LLM as bounded nondeterminism over a finite set of decisions, and represent tools, approvals, and message failures as explicit environment actions. Avoid modeling prompt text; capture control state, tool state, and approval state instead.

Without fairness assumptions, infinite stuttering is allowed, so eventual progress cannot be guaranteed. Add weak or strong fairness to specific sub-actions only after safety is stable, and only when the real system justifies the scheduling assumption.