From correctless
Generates Alloy formal models of security-relevant behaviors like state machines, protocols, and trust boundaries, then runs Alloy Analyzer to detect design bugs before coding. Use after /cspec.
npx claudepluginhub joshft/correctless --plugin correctlessThis skill is limited to using the following tools:
This skill requires effective intensity `critical` or above. Compute effective intensity as `max(project_intensity, feature_intensity)` using the ordering `standard < high < critical`.
Creates isolated Git worktrees for feature branches with prioritized directory selection, gitignore safety checks, auto project setup for Node/Python/Rust/Go, and baseline verification.
Executes implementation plans in current session by dispatching fresh subagents per independent task, with two-stage reviews: spec compliance then code quality.
Dispatches parallel agents to independently tackle 2+ tasks like separate test failures or subsystems without shared state or dependencies.
This skill requires effective intensity critical or above. Compute effective intensity as max(project_intensity, feature_intensity) using the ordering standard < high < critical.
workflow.intensity from .correctless/config/workflow-config.json (project_intensity). If absent, default to standard..correctless/hooks/workflow-advance.sh status and read the Intensity: line (feature_intensity). If absent, use project_intensity alone.max(project_intensity, feature_intensity).Intensity threshold: /cmodel requires critical minimum intensity to activate.
--force to override the intensity gate, or set workflow.intensity to critical in .correctless/config/workflow-config.json--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.
Features that involve: state machines, protocol handling, access control, trust boundary transitions, resource ownership. Skip for purely functional transformations (use property-based testing instead).
Formal modeling takes 10-15 minutes, with the Alloy Analyzer potentially running 30+ seconds per assertion. The user must see progress throughout.
Before starting, create a task list:
Between each step, print a 1-line status: "Modelable scope identified — {N} state machines, {M} trust boundaries. Generating Alloy model..." When the analyzer runs, announce each assertion: "Checking {assertion} (INV-xxx)..." If auto-retrying syntax errors: "Syntax error — fixing and retrying (attempt {N}/3)..." When the interpreter subagent completes, announce: "Interpreter complete — {N} counterexamples translated to domain scenarios."
Mark each task complete as it finishes.
Check current phase: .correctless/hooks/workflow-advance.sh status. You should be in the model phase. If not, tell the human to run /cspec first to enter the correct phase. Do not advance state from the wrong phase.
.correctless/ARCHITECTURE.md for existing trust boundaries and abstractions..correctless/config/workflow-config.json for the Alloy JAR path.Not everything needs modeling. Focus on:
Skip: data transformations, config validation, numeric calculations.
Write to docs/models/{task-slug}.also. Use Alloy 6 syntax.
Every assertion MUST reference the spec invariant ID it encodes (e.g., // INV-003).
java -jar {alloy_jar} {model_file}
For each assertion, run check assertionName for N (start with scope 5).
Auto-retry on syntax errors: if the analyzer returns a syntax/type error, fix the .also file and re-run. Up to 3 retries before surfacing to the human.
Do NOT interpret counterexamples yourself. You wrote the model — you have blind spots. Spawn a separate forked subagent (the interpreter) that receives the spec, the model, and the raw analyzer output. It translates counterexamples to domain-specific scenarios.
Interpreter subagent prompt:
You are the Alloy model interpreter. You did NOT write this model. Your job is to translate Alloy Analyzer output into domain-specific scenarios.
You receive:
- The feature spec (read from .correctless/specs/{task-slug}.md)
- The Alloy model (read from docs/models/{task-slug}.also)
- The raw Alloy Analyzer output
For each counterexample trace:
- Map abstract Alloy states to concrete system behavior
- Translate the trace into a step-by-step scenario in domain terms
- Identify which spec invariant (INV-xxx) is violated
- Present BOTH the raw Alloy trace AND your interpretation — the human verifies the translation
If a counterexample looks like a modeling error (the model allows behavior the real system doesn't), say so explicitly — don't force a domain interpretation of a model bug.
Use Read to examine the spec and model files. Return your interpretation as your final text response.
Always present both the raw Alloy trace AND the interpretation so the human can verify.
If counterexamples found: map to INV-xxx/PRH-xxx, propose spec revisions. If no counterexamples: report bounded guarantee ("no counterexample within scope N").
Ask: "Does this model accurately represent the feature? Are there behaviors I missed?"
This is load-bearing. A correct analysis of a wrong model creates false confidence.
Write analysis results to docs/models/{task-slug}-results.md.
.correctless/hooks/workflow-advance.sh review-spec
After advancing, tell the human: "Model complete. Run /creview-spec for multi-agent adversarial review of the spec."
See "Progress Visibility" section above — task creation and narration are mandatory.
After the interpreter subagent completes, capture total_tokens and duration_ms from the completion result. Append an entry to .correctless/artifacts/token-log-{slug}.json (derive slug from the task slug):
{
"skill": "cmodel",
"phase": "interpreter",
"agent_role": "interpreter-agent",
"total_tokens": N,
"duration_ms": N,
"timestamp": "ISO"
}
If the file doesn't exist, create it with the first entry. /cmetrics aggregates from raw entries — no totals field needed.
Run the Alloy Analyzer (java -jar) as a background task while preparing the counterexample interpretation context. The JAR can take 30+ seconds for complex state spaces.
/cstatus to see where you are. Use workflow-advance.sh override "reason" if the gate is blocking legitimate work.always, after, until) is inconsistent for complex formulas.