alloy-structural-analysislisted

Formal model-checking layer over Allium specs using Alloy 6 + Electrod + nuXmv. Trigger on: "rigorous structural analysis", "model-check this spec", "verify this Allium spec formally", "check for structural divergence with Alloy", "run the Alloy loop", "does the code actually satisfy this spec", temporal/CTL/LTL property checking on a spec, or when weed/allium surface a divergence that needs a deeper formal check than pattern-matching can give. Translates Allium spec obligations into Alloy models, invokes electrod.nuxmv for real temporal model-checking (not Alloy's default bounded SAT backend), parses receipt.json/stdout for verdicts, and on a genuine counterexample hands off to ast-grep/serena to locate the corresponding code. Do not use for spec-vs-code divergence without a formal-verification need (use `weed`), for parsing/checking Allium syntax alone (use `allium check`/`model`/`plan` directly), or for structural code search with no spec/model angle (use `ast-grep`/`serena` directly).
tkolleh/skills · ★ 1 · Data & Documents · score 78

Install: claude install-skill tkolleh/skills

# Alloy Structural Analysis A formal model-checking layer over Allium specs. Where `allium check` validates that a spec parses and is self-consistent, and `weed` compares a spec against the code by pattern and judgment, this skill adds the one thing neither does: exhaustively searching a spec's actual state space with Alloy, Electrod, and nuXmv for a counterexample to a claimed property. An `UNSAT` result here is a much stronger claim than "the tests pass" — it means no state satisfying the negated property exists within the checked scope, not just that no one has found one yet. This skill does one thing well and hands off the rest. It does not parse Allium syntax (`allium` already does), does not judge spec-vs-code divergence (`weed` already does), and does not search code (`ast-grep`/`serena` already do). Its job is the translation into Alloy and the model-checking run in between. Work phases **A → F** in order. C and D can loop back into B for a narrowed re-check — see Phase F. --- ## Phase A — Scope Establish exactly which Allium spec(s) and which codebase area are in scope before doing anything else. 1. Identify the spec file(s) or obligation(s) under analysis. If the user named a PR, ticket, or divergence already surfaced by `weed`, scope to the obligation that divergence concerns — not the whole spec. 2. Identify the codebase area Phase E will search, if a counterexample surfaces. Ask if ambiguous; do not assume the whole repo is in scope just because a spec fil