How do I install the Tla Refinement Proofs skill?

Run npx skillmds@latest add photoszzt/tla-refinement-proofs in your terminal (requires Node.js), paste this page's agent-chat prompt into Claude, Cursor, or any MCP-connected agent, or download the SKILL.md file and copy it into your agent's skills directory.

Is Tla Refinement Proofs safe to use?

This skill has not completed SkillMD's automated safety review yet. Capability flags: docs only. SkillMD never runs a skill's scripts for you; review the SKILL.md before installing.

Which AI agents work with Tla Refinement Proofs?

This skill is tagged as working with Claude Code, Claude.ai, OpenAI Codex. SKILL.md is an open format, so most agents that read a skills directory can load it too.

Is Tla Refinement Proofs free to use?

Yes. Installing skills from SkillMD is free, and the skill stays under its author's original license.

Who published Tla Refinement Proofs?

photoszzt (@photoszzt) published this skill. Their other Agent Skills are listed on their SkillMD profile.

Tla Refinement Proofs by photoszzt — Agent Skill

Name: Tla Refinement Proofs
Rating: 4.666666666666667 (3 reviews)
Author: photoszzt

Tla Refinement Proofs

This skill provides guidance on specification refinement — proving that one TLA+ specification correctly implements another. It should be used when the user asks about "refinement", "specification refinement", "refine specification", "abstract and concrete specs", "implementation correctness", "prove implementation correct", "specification layers", "refinement mapping", "INSTANCE WITH", "TLAPS", "stuttering steps", "data refinement", or mentions proving one spec implements another.

photoszzt Updated Sep 10, 2026

File contents

TLA+ Refinement and Specification Relationships

This skill provides guidance on specification refinement - proving that one specification correctly implements another.

When to Use

Showing implementation refines abstract specification
Verifying concrete spec satisfies abstract properties
Relating high-level and low-level specifications
Proving correctness of optimizations
Understanding refinement mappings

What is Refinement?

Refinement proves that a concrete (implementation) specification correctly implements an abstract (high-level) specification. Every behavior allowed by the concrete spec must correspond to a behavior allowed by the abstract spec.

Why Refine? Layered design, verified implementation, optimization verification, and interface compliance.

Types of Refinement

Safety Refinement: Concrete spec's behaviors are a subset of abstract spec's behaviors. Define a refinement mapping, then check with TLC.

Liveness Refinement: Concrete spec satisfies abstract spec's liveness properties. Requires safety refinement plus fairness conditions.

Refinement Workflow with TLC

1. Create Abstract Specification

---- MODULE AbstractCounter ----
EXTENDS Naturals
VARIABLE count
Init == count = 0
Inc == count' = count + 1
Spec == Init /\ [][Inc]_count
====

2. Create Concrete Specification

---- MODULE ConcreteCounter ----
EXTENDS Naturals
VARIABLES x, y
Init == x = 0 /\ y = 0
IncX == x' = x + 1 /\ UNCHANGED y
IncY == y' = y + 1 /\ UNCHANGED x
Spec == Init /\ [][IncX \/ IncY]_<<x,y>>
====

3. Define Refinement Mapping and Check

In concrete spec, instantiate abstract with mapping:

A == INSTANCE AbstractCounter WITH count <- x + y
THEOREM Spec => A!Spec

4. TLC Configuration

SPECIFICATION Spec
PROPERTY A!Spec

5. Run TLC

/tla-check @QueueRefinement.tla

(Use the path to your refinement spec, e.g., @examples/QueueRefinement.tla)

If passes: concrete refines abstract. If fails: trace shows where refinement breaks.

Quick Reference

---- MODULE Concrete ----
VARIABLES ...concrete vars...
ConcreteSpec == ConcreteInit /\ [][ConcreteNext]_vars

A == INSTANCE Abstract WITH abstractVar <- mappingExpression

THEOREM ConcreteSpec => A!Spec
====

Best Practices

Verify concrete spec correct on its own first
Check type refinement, then safety, then liveness
Comment refinement mappings clearly
Chain refinements for complex systems (Spec0 -> Spec1 -> Spec2)

Reference Files

references/refinement-patterns.md - Complete refinement mapping patterns (state mapping, history variables, stuttering steps, data/protocol/state machine refinement)
references/checking-refinement.md - Verifying refinement with TLC, diagnosing failures, TLC vs TLAPS comparison
references/tlaps-guide.md - TLAPS proof system guide (advanced)

Examples

See examples/ directory: AbstractQueue.tla, ConcreteQueue.tla, QueueRefinement.tla

Related Skills

tla-model-checking - Run TLC checks
tla-getting-started - TLA+ basics
tla-debug-violations - Debug counterexamples
/tla-check - Verify refinement
/tla-review - Review refinement structure

---name: tla-refinement-proofsdescription: This skill provides guidance on specification refinement — proving that one TLA+ specification correctly implements another. It should be used when the user asks about "refinement", "specification refinement", "refine specification", "abstract and concrete specs", "implementation correctness", "prove implementation correct", "specification layers", "refinement mapping", "INSTANCE WITH", "TLAPS", "stuttering steps", "data refinement", or mentions proving one spec implements another.---# TLA+ Refinement and Specification RelationshipsThis skill provides guidance on specification refinement - proving that one specification correctly implements another.## When to Use- Showing implementation refines abstract specification- Verifying concrete spec satisfies abstract properties- Relating high-level and low-level specifications- Proving correctness of optimizations- Understanding refinement mappings## What is Refinement?**Refinement** proves that a concrete (implementation) specification correctly implements an abstract (high-level) specification. Every behavior allowed by the concrete spec must correspond to a behavior allowed by the abstract spec.**Why Refine?** Layered design, verified implementation, optimization verification, and interface compliance.## Types of Refinement**Safety Refinement**: Concrete spec's behaviors are a subset of abstract spec's behaviors. Define a refinement mapping, then check with TLC.**Liveness Refinement**: Concrete spec satisfies abstract spec's liveness properties. Requires safety refinement plus fairness conditions.## Refinement Workflow with TLC### 1. Create Abstract Specification```tla---- MODULE AbstractCounter ----EXTENDS NaturalsVARIABLE countInit == count = 0Inc == count' = count + 1Spec == Init /\ [][Inc]_count====```### 2. Create Concrete Specification```tla---- MODULE ConcreteCounter ----EXTENDS NaturalsVARIABLES x, yInit == x = 0 /\ y = 0IncX == x' = x + 1 /\ UNCHANGED yIncY == y' = y + 1 /\ UNCHANGED xSpec == Init /\ [][IncX \/ IncY]_<<x,y>>====```### 3. Define Refinement Mapping and CheckIn concrete spec, instantiate abstract with mapping:```tlaA == INSTANCE AbstractCounter WITH count <- x + yTHEOREM Spec => A!Spec```### 4. TLC Configuration```SPECIFICATION SpecPROPERTY A!Spec```### 5. Run TLC```/tla-check @QueueRefinement.tla```(Use the path to your refinement spec, e.g., `@examples/QueueRefinement.tla`)If passes: concrete refines abstract. If fails: trace shows where refinement breaks.## Quick Reference```tla---- MODULE Concrete ----VARIABLES ...concrete vars...ConcreteSpec == ConcreteInit /\ [][ConcreteNext]_varsA == INSTANCE Abstract WITH abstractVar <- mappingExpressionTHEOREM ConcreteSpec => A!Spec====```## Best Practices1. Verify concrete spec correct on its own first2. Check type refinement, then safety, then liveness3. Comment refinement mappings clearly4. Chain refinements for complex systems (Spec0 -> Spec1 -> Spec2)## Reference Files- **`references/refinement-patterns.md`** - Complete refinement mapping patterns (state mapping, history variables, stuttering steps, data/protocol/state machine refinement)- **`references/checking-refinement.md`** - Verifying refinement with TLC, diagnosing failures, TLC vs TLAPS comparison- **`references/tlaps-guide.md`** - TLAPS proof system guide (advanced)## ExamplesSee `examples/` directory: `AbstractQueue.tla`, `ConcreteQueue.tla`, `QueueRefinement.tla`## Related Skills- `tla-model-checking` - Run TLC checks- `tla-getting-started` - TLA+ basics- `tla-debug-violations` - Debug counterexamples- `/tla-check` - Verify refinement- `/tla-review` - Review refinement structure

Frequently asked questions