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.
npx claudepluginhub younes-io/agent-skillsThis skill uses the workspace's default tool permissions.
- Updated proof-bearing TLA+ module(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.
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.
Share bugs, ideas, or general feedback.
*.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 ideas