From tla-workbenches
Writes and iteratively refines TLA+ theorem proofs in .tla modules with TLAPS; runs proof checks and summarizes proved vs failed/omitted obligations. Use for THEOREM/PROOF blocks, diagnosing failures, invariants, equivalence.
How this skill is triggered — by the user, by Claude, or both
Slash command
/tla-workbenches:tla-proofThe summary Claude sees in its skill listing — used to decide when to auto-load this skill
- Updated proof-bearing TLA+ module(s): `*.tla`
*.tla.tla-proof/runs/<run-id>/...ASSUME, AXIOM, omitted proofs, imported facts).Record:
If theorem intent is ambiguous, state candidate interpretations and choose one explicitly.
If the user is refactoring a spec and wants semantic preservation, consider a direct equivalence theorem (F <=> G) instead of only bounded TLC evidence.
Start with the smallest stable structure:
THEOREM ...PROOFSUFFICES, HAVE, CASE, PICK, TAKE, WITNESS, QED as neededPrefer explicit sub-lemmas over long single-step BY clauses.
Use BY DEF ... only for required definitions.
Formula-equivalence proofs for refactors are a supported pattern, for example THEOREM F <=> G BY DEF F, G.
Match the structure to the proof class:
Next by actionTHEOREM F <=> G; if a one-line proof fails, split into F => G and G => FPrereqs:
bashjqtlapmRun from the skill directory:
scripts/tlaps_check.sh --spec path/to/Foo.tla
Artifacts:
.tla-proof/runs/<run-id>/summary.json.tla-proof/runs/<run-id>/tlaps.stdout.tla-proof/runs/<run-id>/tlaps.stderrClassify failures before editing:
Patch minimally, then re-run. If the same inductive step keeps failing, stop cycling tactics and propose the smallest strengthening fact that would make the step go through.
Report:
If counts are inconclusive, say so explicitly.
Common refactor-proof target: prove a rewritten formula or action is equivalent to the original, rather than only model-checking F <=> G with TLC.
scripts/tlaps_check.sh: run tlapm, capture logs, emit summary.jsonreferences/proof_skeleton.md: minimal hierarchical proof templatesreferences/local_moves.md: TLAPS-specific logical moves and proof-shape defaultsreferences/proof_debugging.md: failure taxonomy and remediation playbookreferences/tactics_quickref.md: tactic/backend guidance and escalation orderreferences/case_bank.md: discussion-derived proof classes and non-trivial example ideasnpx claudepluginhub younes-io/agent-skillsGuides TLA+ formal verification of concurrent/distributed designs using PlusCal and TLC, complementing PBT for implementation. Use for protocol correctness and state risks.
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.
Orchestrates collaborative theorem proving in Lean using lc CLI for state management and parallel agents. Employs skeleton verification, math cards, and architecture planning for complex goals.