Alloy 6

Create models that expose assumptions and find counterexamples. Treat Analyzer results as evidence over declared bounds, not as an automatic proof of the real system.

Load only the references needed

• Read relational-modeling.md for every authoring, explanation, or review task.
• Read temporal-modeling.md when anything changes over time or the model uses var, prime, temporal operators, actions, or traces.
• Read analysis-debugging.md before executing commands, interpreting results, debugging an unsatisfiable model, or making a verification claim.
• Read maintenance-existing-models.md when repairing a model from an issue, paper, standard, accepted patch, or Analyzer XML instance, especially when the requested change must remain narrow.
• Read legacy-migration.md for pre-6 models, util/ordering[State], or Alloy 4-to-6 migration.
• Read security-modeling.md for authentication, authorization, capabilities, attacker knowledge, or adversarial modeling.
• Read sources.md when provenance, version routing, or further study matters.

Use structural-access.als, temporal-capability.als, and protocol-events.als as small syntax patterns, not domain requirements.

Correctness contract

Keep these four things visibly separate: