菜单
Detect when implementation code has changed but its formal TLX spec has not been updated. Compares git timestamps, re-extracts structure, and diffs against existing specs. Use when asked to check spec drift, detect stale specs, verify specs are up to date, or audit spec freshness.
用 Codex 或 Claude 帮你安装 复制这段 Prompt，粘贴到 Codex、Claude 或其他助手里，让它检查 Skill 页面并帮你完成安装。
Formal specification workflow for state machines using TLX (TLA+ in Elixir). Covers writing abstract specs from ADRs, generating concrete specs from code, enriching extracted skeletons with invariants and properties, refinement checking, and CI integration. Use when asked to write a spec, formally specify, verify a state machine, check refinement, generate a concrete spec, enrich a skeleton, or compare abstract and concrete specs.
Scan an Elixir/Erlang project for modules that TLX can formally specify. Covers OTP behaviours (GenServer, gen_statem, LiveView), framework extensions (Ash.StateMachine), and workflow/pipeline libraries (Reactor, Broadway). Reports spec coverage and suggests where to focus verification effort. Use when asked to audit, scan, find extractable modules, check spec coverage, or triage formal verification targets.
Generate state machine diagrams from TLX specs in multiple formats (DOT, Mermaid, PlantUML, D2). Use when asked to visualize a spec, generate a diagram, draw a state machine, create a graph, or render a spec as an image.
Use this skill when building or modifying the Spark DSL extension. Consult for entity definitions, sections, transformers, and verifiers.
基于 SOC 职业分类
| name | spec-drift |
| description | Detect when implementation code has changed but its formal TLX spec has not been updated. Compares git timestamps, re-extracts structure, and diffs against existing specs. Use when asked to check spec drift, detect stale specs, verify specs are up to date, or audit spec freshness. |
| license | MIT |
| metadata | {"author":"jrjsmrtn","version":"0.1.0"} |
Detect when implementation code has diverged from its formal TLX spec, so specs stay in sync with the codebase.
Scan for spec files that declare a # Source: header:
grep -rl "# Source:" specs/ lib/specs/ test/specs/
For each spec file, extract:
# Source: path (implementation file)# ADR: number (if present)For each spec/source pair, check git modification dates:
# Last modification of source
git log -1 --format="%ai" -- lib/my_app/reconciler.ex
# Last modification of spec
git log -1 --format="%ai" -- specs/reconciler_spec.ex
If the source is newer than the spec, the spec may be stale.
For stale specs, re-run the appropriate extractor and compare the extracted structure against the existing spec:
# Re-extract current structure
mix tlx.gen.from_gen_server MyApp.Reconciler --format codegen --output /tmp/current.ex
# Diff against existing spec
diff specs/reconciler_spec.ex /tmp/current.ex
Look for:
Present findings as a table:
Spec Source Status
──────────────────────────────────────────────────────────────────────
specs/reconciler_spec.ex lib/my_app/reconciler.ex ⚠ STALE
Source modified: 2026-03-28 Spec modified: 2026-03-15
Diff: +2 new handle_call clauses, +1 new field (retry_count)
specs/orchestrator_spec.ex lib/my_app/orchestrator.ex ✓ OK
Source modified: 2026-03-10 Spec modified: 2026-03-12
specs/fleet_live_spec.ex lib/my_app_web/fleet_live.ex ⚠ STALE
Source modified: 2026-03-25 Spec modified: 2026-03-01
Diff: +3 new handle_event clauses
──────────────────────────────────────────────────────────────────────
Stale: 2/3 Up to date: 1/3
For each stale spec:
Direct the user to the formal-spec skill's Phase 2B (enrichment)
for any new actions or fields that need invariants.
Add to a pre-push hook or CI step:
# Simple timestamp check
for spec in specs/*_spec.ex; do
source=$(grep "# Source:" "$spec" | sed 's/# Source: //')
if [ -n "$source" ] && [ "$source" -nt "$spec" ]; then
echo "STALE: $spec (source: $source)"
exit 1
fi
done
For deeper structural comparison, use the extractor diff approach from Step 3 in a Mix task or test.