tla-modellisted

Models concurrent and distributed designs in TLA+ or PlusCal and checks them with the TLC model checker. Use when asked to write, review, or debug a TLA+ spec, .tla/.cfg files, or TLC output, or to model-check or formally verify a protocol, lock, lease, consensus, replication, WAL, retry, or race condition. Do NOT use for unit or property-based tests (use test-writing) or for Lean, Coq, Dafny, or Verus proofs.
wilbeibi/wilbeibi-skills · ★ 2 · AI & Automation · score 78

Install: claude install-skill wilbeibi/wilbeibi-skills

# tla-model The deliverable is a checked argument, not a `.tla` file: every property traces to a requirement, every action to an implementation event, and every green result survives mutation. TLC finding nothing means *no counterexample in this model at these bounds*; never call it a proof. ## Setup ```bash scripts/tlc.py check examples/MiniLock.tla -c examples/MiniLock.cfg # expect "result: clean", exit 0 scripts/tlc.py fetch # if tla2tools.jar is missing; or set TLA2TOOLS_JAR ``` Missing Java: ask the user to install a JRE 11+; do not download one. `scripts/test_tlc.sh` self-tests the helper. PlusCal: run `scripts/tlc.py translate Spec.tla` before every check. `tlc.py check` prints result, state counts, per-action coverage, the full trace, and `VACUITY:` flags. Exit 0 clean, 1 violation, 2 vacuous, 3 setup/parse error. `tlc.py mutant` applies one exact-match edit to a copy and exits 0 only when the named property catches it (`KILLED`). A question about an existing spec or TLC output needs only `check` and the matching step below. Create files only when asked to model or verify a system. Keep that work in `spec/` beside the code: `modeling-brief.md`, `<Name>.tla`, one cfg per concern, `cex/`, `report.md`. ## Loop 1. **Brief before spec.** Fill [BRIEF-TEMPLATE.md](BRIEF-TEMPLATE.md) into `spec/modeling-brief.md`. Aim the question where bugs have lived: search `git log` and the issue tracker for fix, race, crash, deadlock, corrupt, and stale on the core f