skills.rest
photoszzt
photoszztCOMMUNITY
Explore all skills by this author →
GitHub

tla-refinement-proofs

Verify TLA+ specification refinement using TLC model checking.

Updated Jan 27, 2026
Search Tags:#refinement#specification#verification#tla+#model checking#tlaps
One-click install
npx skills add https://github.com/photoszzt/tlaplus-ai-tools --skill tla-refinement-proofs
Or copy as Structured Prompt for Agent▼
Please help me install this Agent Skill.
Skill: tla-refinement-proofs
Source: https://github.com/photoszzt/tlaplus-ai-tools/tree/main/skills/tla-refinement-proofs
Command: npx skills add https://github.com/photoszzt/tlaplus-ai-tools --skill tla-refinement-proofs

SYSTEM DOCUMENTATION & REQUIREMENTS

💡 This Skill includes references (resource) components.

What problem does it solve?

This Skill helps users understand and verify that a detailed, concrete TLA+ specification correctly implements a higher-level, abstract specification, ensuring implementation correctness.

Core Features & Use Cases

  • Refinement Mapping: Define how variables and states in a concrete spec correspond to an abstract spec.
  • Safety & Liveness Verification: Use TLC to check if concrete behaviors are a subset of abstract behaviors and satisfy liveness properties.
  • Use Case: You've designed a complex distributed system at a high level and now have a detailed implementation. This skill guides you to prove that your implementation adheres to the original abstract design using TLA+ tools.

Quick Start

Use the tla-refinement-proofs skill to check if the concrete counter example spec implements the abstract counter example spec.

Frequently Asked Questions about tla-refinement-proofs

High-intent search queries and answers about installing and using this skill.

FAQPage Schema
How do I prove a concrete TLA+ specification implements an abstract design?▼

To prove a concrete TLA+ specification implements an abstract design, you establish a refinement mapping that links concrete variables to abstract states, then use TLC to verify safety and liveness properties hold.

What is refinement mapping in TLA+ and when do I need it?▼

Refinement mapping in TLA+ defines how variables and states in a concrete specification correspond to an abstract specification. You need it to verify that detailed implementation behaviors are a subset of abstract design behaviors.

Can TLC verify both safety and liveness properties during TLA+ refinement checking?▼

Yes, TLC can verify both safety and liveness properties during TLA+ refinement checking by ensuring concrete behaviors satisfy the abstract specification's invariants and temporal properties.

How do I check data and protocol refinement patterns using TLA+ specifications?▼

You check data, protocol, and state machine refinement patterns in TLA+ by defining abstract and concrete specifications, establishing a refinement mapping between them, and running TLC model checking.

What are the common refinement patterns supported in TLA+ verification?▼

Common refinement patterns supported in TLA+ verification include data refinement, protocol refinement, and state machine refinement, all verified using TLC to ensure concrete specs correctly implement abstract specifications.

Why does my TLA+ refinement proof fail when checking liveness properties with TLC?▼

TLA+ refinement liveness proofs fail with TLC when concrete behaviors do not satisfy the abstract specification's temporal properties, often caused by an incorrect refinement mapping or missing fairness conditions in the concrete spec.

Related Skills

Explore More Software Engineering Skills→
santosomarsantosomar
1

tlaplus-spec-generator

Generate TLA+ specifications from natural language or pseudocode descriptions.

Community
Advanced
dtsongdtsong
1

tlaplus-security-skill

Generate TLA+ specifications and TLC configurations for formal security verification.

Community
Advanced
v1bh0rv1bh0r

nw-formal-verification-tlaplus

Specify and verify distributed system invariants with TLA+/PlusCal.

Community
Advanced
ArabelaTsoArabelaTso
142

proof-failure-explainer

Analyze and explain formal verification proof failures in Isabelle and Coq.

Community
Intermediate