From tla-workbenches
Writes and refines TLA+ specs (.tla) and TLC configs (.cfg) from natural-language designs; runs model checking; summarizes results, counterexamples, and assumptions. For protocol/state machine validation.
npx claudepluginhub younes-io/agent-skillsThis skill uses the workspace's default tool permissions.
- TLA+ spec(s): `*.tla`
Guides TLA+ formal verification of concurrent/distributed designs using PlusCal and TLC, complementing PBT for implementation. Use for protocol correctness and state risks.
Provides TLA+ templates, syntax guidance, type invariants, and best practices for specifying distributed systems and concurrent algorithms. Useful for formal design and verification with TLC.
Guides Next.js Cache Components and Partial Prerendering (PPR): 'use cache' directives, cacheLife(), cacheTag(), revalidateTag() for caching, invalidation, static/dynamic optimization. Auto-activates on cacheComponents: true.
Share bugs, ideas, or general feedback.
*.tla*.cfg.tla-check/runs/<run-id>/... (logs, json trace if any)WF_/SF_), or explicitly say "none (safety-only run)".CONSTRAINT / ACTION_CONSTRAINT, list each one and the behavior it excludes.Ask for (and record) answers:
WF_/SF_)If the user doesn't specify bounds, propose minimal ones (and label them as "proposed"):
Use a consistent structure:
CONSTANTS for bounded sets (e.g., Nodes, Values).VARIABLES for state.Vars == <<...>> as a single canonical variable tuple name. Use the same casing (Vars) everywhere.TypeOK (type invariant) to keep the model honest.Init and Next (with UNCHANGED for untouched vars).Spec == Init /\\ [][Next]_Vars.Spec with explicit fairness assumptions, e.g. /\\ WF_Vars(SomeAction) or /\\ SF_Vars(SomeAction)..cfg.Prefer modeling the design over implementation details. If the design is fuzzy, model the uncertainty explicitly with nondeterminism and constraints.
Maintain a compact checklist that maps each natural-language requirement to one of:
.cfg).cfg)When reporting results, include this ledger (or a short version) so it's obvious what passed vs what was never encoded.
.cfg (Make the Model Check Run)Baseline config (edit as needed):
SPECIFICATION Spec
\* Or:
\* INIT Init
\* NEXT Next
CONSTANTS
\* Example:
\* Nodes = {n1, n2, n3}
\* Values = {v1, v2}
INVARIANT
TypeOK
\* Add safety invariants here
CHECK_DEADLOCK TRUE
Deadlock policy:
CHECK_DEADLOCK TRUE by default.If you introduce CONSTRAINT / ACTION_CONSTRAINT, call it out as a coverage tradeoff and report what behavior it removes.
Prereqs:
java on PATHjq on PATHtla2tools.jar available and pointed to by TLA2TOOLS_JAR (or pass --jar)Run (from the tla-check skill directory):
scripts/tlc_check.sh --spec path/to/Foo.tla --cfg path/to/Foo.cfg
This writes a run directory under the spec folder:
.tla-check/runs/<run-id>/summary.json.tla-check/runs/<run-id>/tlc.stdout.tla-check/runs/<run-id>/tlc.stderr.tla-check/runs/<run-id>/counterexample.json (only if TLC produced one)If TLC fails:
If TLC passes:
scripts/tlc_check.sh: run TLC with -dumpTrace json, capture logs, emit summary.jsonscripts/tlc_trace_summary.sh: summarize a counterexample.json into step-by-step diffs (optional helper)references/spec_skeleton.md: minimal skeleton patterns and cfg snippets