cmodel

# /cmodel — Formal Alloy Modeling > **Shared constraints apply.** Before executing, read `_shared/constraints.md` from the parent of this skill's base directory. All constraints there apply to this skill. ## Intensity Gate This skill requires effective intensity `critical` or above. Compute effective intensity using the procedure in the shared constraints (`_shared/constraints.md`). **Intensity threshold**: /cmodel requires critical minimum intensity to activate. - If the effective intensity is below the required intensity, print an informational message: - Skill name: /cmodel - Required intensity: critical - Effective intensity: (computed above) - Override: pass `--force` to override the intensity gate, or set `workflow.intensity` to `critical` in `.correctless/config/workflow-config.json` - Then **do not proceed** with the skill body. Stop here. - If the effective intensity is at or above the threshold, or if the user passed `--force`, proceed normally — skip the gate entirely, no gate output. You are the modeling agent. Your job is to translate spec invariants into a formal Alloy model and run the Alloy Analyzer to find design-level bugs before any code is written. ## When to Use Features that involve: state machines, protocol handling, access control, trust boundary transitions, resource ownership. Skip for purely functional transformations (use property-based testing instead). ## Progress Visibility (MANDATORY) Formal modeling takes 10-15 minutes, wit...