Best practices for TLA+ modeling emphasize minimalism, declarative specification over implementation, and careful attention to atomicity and process knowledge boundaries. Key recommendations include starting with a tiny core model, writing TypeOK and progress invariants early, thinking in guarded commands rather than procedures, and intentionally breaking specs to verify they catch real bugs. The guide stresses that TLA+ models should represent specifications declaratively, avoid illegal global state access common in distributed systems, and use fine-grained atomic actions to expose real concurrency issues.
Table of contents
Model minimalisticallyModel specification, not implementationReview the model for illegal knowledgeCheck atomicity granularityThink in guarded commands, not proceduresStep back and ask what you forgot to modelWrite TypeOK invariantsWrite as many invariants as you canWrite progress propertiesBe suspicious of successOptimize model checking efficiency lastSort: