Add TLA+ Specification Review Guidelines

[lemmy]

• Introduced a new document outlining best practices for reviewing and validating TLA+ specifications.
• Covers key areas such as model checking, simulation, specification structure, constants, variables, invariants, properties, fairness constraints, and documentation standards.
• Provides a systematic approach for reviewers to evaluate TLA+ specifications using a producer-consumer example.

This is based on three sources:
a) items that came to mind while reviewing the project
b) material that Claude Sonnet 4.5 extracted from old PR at https://github.com/tlaplus/Examples/pulls
c) discussions that Claude Sonnet 4.5 gathered from https://discuss.tlapl.us/

[Documentation]

[lemmy]

Inviting TLA+ experts like @hwayne @muenchnerkindl @will62794, @kape1395, @craft095, @ajdavis, @muratdem, @konnov, ... to contribute their review guidelines and checklist items.

[lemmy]

@muenchnerkindl Thank you (all suggestions have been incorporated)!

[konnov]

Who is the audience of this document? It looks like it is being designed for LLMs. I find the lack of structure in this document rather confusing.

[lemmy]

@konnov What other structure are you suggesting? It starts with a section on guidelines of formulas, followed by sections for each section of a TLA+ spec, ending with at section how to do (TLC) model checking.

[konnov]

@konnov What other structure are you suggesting? It starts with a section on guidelines of formulas, followed by sections for each section of a TLA+ spec, ending with at section how to do (TLC) model checking.

I am trying to understand the current structure at the moment. Perhaps, it is the section "Functions, Records, and Sequences" that threw me off, as it focuses on one particular language feature. The following sections on the specification structure look much more complete.

[lemmy]

I am trying to understand the current structure at the moment. Perhaps, it is the section "Functions, Records, and Sequences" that threw me off, as it focuses on one particular language feature. The following sections on the specification structure look much more complete.

Yes, the initial section currently contains only this one item, which gives it an unstructured appearance. However, I intend to add more items to the section over time.

[lemmy]

@konnov Is your review still pending, or can I proceed with the PR?

[konnov]

Yes, the initial section currently contains only this one item, which gives it an unstructured appearance. However, I intend to add more items to the section over time.

Please go ahead and merge it. I don't want to block your PR.