TLA+ Specification Review

Run a comprehensive review of your TLA+ specification including parsing, symbol extraction, smoke testing, and best practices checklist.

IMPORTANT: Always use the MCP tools listed above. Never fall back to running Java or TLC commands via Bash.

Usage

/tla-review test-specs/Counter.tla
/tla-review test-specs/Counter.tla test-specs/Counter.cfg
/tla-review test-specs/Counter.tla --no-smoke

Note: If you typed

@path.tla

as the first argument, this skill strips the leading

@

and validates the file exists.

What This Does

1. Validates and normalizes the spec path from the argument
2. Runs SANY parser to check syntax and semantics
3. Extracts symbols to analyze spec structure
4. Runs smoke test (unless

   --no-smoke

   flag present)
5. Generates comprehensive review report with recommendations

Implementation

Step 1: Normalize Spec Path

Take the spec file path provided as the argument to this skill. If it starts with

@

, strip the leading

@

.

Print

Spec path: <spec_path>

Step 2: Validate File

• Check path ends with

  .tla

• Use the Read tool to verify the file exists on disk
• If validation fails, print error and exit

Step 3: Parse Flags

Extract flags from the argument:

• --no-smoke

  : Skip smoke test (default: smoke enabled)

Step 4: Determine CFG Argument

Parse the second token from the argument (split by space, take second). If it ends with

.cfg

, treat it as the CFG_ARG.

Step 5: Run SANY Parser

Call

mcp__plugin_tlaplus_tlaplus__tlaplus_mcp_sany_parse

with

fileName=<spec_path>

Store result:

• PARSE_SUCCESS=true/false

• PARSE_ERRORS=<error list>

Step 6: Extract Symbols

Call

mcp__plugin_tlaplus_tlaplus__tlaplus_mcp_sany_symbol

with:

• fileName=<spec_path>

• includeExtendedModules=false

Store result:

• SYMBOLS=<symbol extraction result>

• Extract:

  CONSTANTS

  ,

  VARIABLES

  ,

  INIT

  ,

  NEXT

  ,

  SPEC

  ,

  INVARIANTS

  ,

  PROPERTIES

Step 7: Run Smoke Test (if enabled)

If smoke is enabled (no

--no-smoke

flag):

Apply CFG selection algorithm (same as

/tla-smoke

):

Phase 1: Ensure precondition

Extract spec name and directory:

SPEC_DIR = dirname(SPEC_PATH)
SPEC_NAME = basename(SPEC_PATH, .tla)

Check preconditions in order:

1. If

   SPEC_DIR/SPEC_NAME.cfg

   exists:
   • Print

     Phase 1: Spec.cfg exists

   • Precondition satisfied

2. Else if

   SPEC_DIR/MC<SPEC_NAME>.tla

   AND

   SPEC_DIR/MC<SPEC_NAME>.cfg

   both exist:
   • Print

     Phase 1: MC pair exists

   • Precondition satisfied

3. Else if

   CFG_ARG

   is non-empty and exists:
   • Copy

     CFG_ARG

     to

     SPEC_DIR/SPEC_NAME.cfg

     (non-clobbering)
   • Print

     Phase 1: Copied cfgArg to SPEC_NAME.cfg

   • Precondition satisfied

4. Else if

   SPEC_DIR/SPEC_NAME.generated.cfg

   exists:
   • Copy it to

     SPEC_DIR/SPEC_NAME.cfg

     (non-clobbering)
   • Print

     Phase 1: Copied generated cfg

   • Precondition satisfied

5. Else:

   • Print

     Smoke test skipped: No config file found

   • Set

     SMOKE_SKIPPED=true

   • Continue to review

Phase 2: Choose cfg

If precondition satisfied:

1. If

   CFG_ARG

   is non-empty:
   • Resolve and use

     CFG_ARG

     (copy if needed, same as

     /tla-smoke

     )
   • Print

     Phase 2: Using explicit cfgArg

2. Else:

   • Use default cfg (

     Spec.cfg

     or

     MCSpec.cfg

     )
   • Print

     Phase 2: Using default cfg

Store final cfg path in

FINAL_CFG

.

Call

mcp__plugin_tlaplus_tlaplus__tlaplus_mcp_tlc_smoke

with:

• fileName=<SPEC_PATH>

• cfgFile=<FINAL_CFG>

• extraJavaOpts=["-Dtlc2.TLC.stopAfter=3"]

Store result:

• SMOKE_SUCCESS=true/false

• SMOKE_VIOLATIONS=<violation list>

Step 8: Generate Review Report

Print comprehensive review summary:

═══════════════════════════════════════════════════════════
TLA+ SPECIFICATION REVIEW
═══════════════════════════════════════════════════════════

Spec: <SPEC_PATH>

─────────────────────────────────────────────────────────
1. SYNTAX & SEMANTICS (SANY Parser)
─────────────────────────────────────────────────────────

<if PARSE_SUCCESS>
Parsing successful. No syntax errors.
<else>
Parsing failed. Errors found:
<PARSE_ERRORS>
<endif>

─────────────────────────────────────────────────────────
2. STRUCTURE ANALYSIS (Symbol Extraction)
─────────────────────────────────────────────────────────

Constants: <CONSTANTS or "None">
Variables: <VARIABLES or "None">
Init: <INIT or "Not detected">
Next: <NEXT or "Not detected">
Spec: <SPEC or "Not detected">
Invariants: <INVARIANTS or "None">
Properties: <PROPERTIES or "None">

<if no INIT or no NEXT or no SPEC>
Warning: Missing behavior specification
  - Ensure Init, Next, and Spec are defined
  - Or define INIT/NEXT in .cfg file
<endif>

<if CONSTANTS non-empty>
Warning: Constants require assignment
  - Edit .cfg file to assign concrete values
  - Example: CONSTANT MaxValue = 10
<endif>

─────────────────────────────────────────────────────────
3. SMOKE TEST (3-second simulation)
─────────────────────────────────────────────────────────

<if SMOKE_SKIPPED>
Skipped (no config file or --no-smoke flag)
<else if SMOKE_SUCCESS>
Smoke test passed
  CFG used: <FINAL_CFG>
  No violations found in random simulation
<else>
Smoke test failed
  CFG used: <FINAL_CFG>
  Violations detected:
<SMOKE_VIOLATIONS>
<endif>

─────────────────────────────────────────────────────────
4. BEST PRACTICES CHECKLIST
─────────────────────────────────────────────────────────

<Check and report on:>

Module documentation
  - Does module have header comment explaining purpose?
  - Are complex operators documented?

Type invariants
  - Are type invariants defined for all variables?
  - Example: TypeInvariant == var \in ExpectedType

Safety properties
  - Are safety invariants defined?
  - Do they cover critical correctness conditions?

Liveness properties
  - Are liveness properties defined if needed?
  - Example: <>[]Termination

Constant bounds
  - Are constants bounded to reasonable values?
  - Large constants cause state explosion

Symmetry
  - Can symmetry sets reduce state space?
  - Example: SYMMETRY SymmetrySet

State constraints
  - Are state constraints needed to limit exploration?
  - Example: CONSTRAINT StateConstraint

─────────────────────────────────────────────────────────
5. RECOMMENDATIONS
─────────────────────────────────────────────────────────

<Generate specific recommendations based on findings:>

<if PARSE_ERRORS>
-> Fix syntax errors before proceeding
<endif>

<if no config file>
-> Run: /tla-symbols <SPEC_PATH>
<endif>

<if CONSTANTS non-empty and no config>
-> Assign constant values in .cfg file
<endif>

<if SMOKE_VIOLATIONS>
-> Fix violations found in smoke test
-> Run: /tla-check for full counterexample
<endif>

<if SMOKE_SUCCESS or SMOKE_SKIPPED>
-> Run: /tla-check for exhaustive verification
<endif>

<if no INVARIANTS>
-> Consider adding type and safety invariants
<endif>

<if no PROPERTIES>
-> Consider adding liveness properties if applicable
<endif>

═══════════════════════════════════════════════════════════
REVIEW COMPLETE
═══════════════════════════════════════════════════════════

Example Output

═══════════════════════════════════════════════════════════
TLA+ SPECIFICATION REVIEW
═══════════════════════════════════════════════════════════

Spec: test-specs/Counter.tla

─────────────────────────────────────────────────────────
1. SYNTAX & SEMANTICS (SANY Parser)
─────────────────────────────────────────────────────────

Parsing successful. No syntax errors.

─────────────────────────────────────────────────────────
2. STRUCTURE ANALYSIS (Symbol Extraction)
─────────────────────────────────────────────────────────

Constants: MaxValue
Variables: count
Init: Init
Next: Next
Spec: Spec
Invariants: TypeInvariant, BoundInvariant
Properties: None

Warning: Constants require assignment
  - Edit .cfg file to assign concrete values
  - Example: CONSTANT MaxValue = 10

─────────────────────────────────────────────────────────
3. SMOKE TEST (3-second simulation)
─────────────────────────────────────────────────────────

Smoke test passed
  CFG used: test-specs/Counter.cfg
  No violations found in random simulation

─────────────────────────────────────────────────────────
4. BEST PRACTICES CHECKLIST
─────────────────────────────────────────────────────────

Module documentation - Header comment present
Type invariants - TypeInvariant defined
Safety properties - BoundInvariant defined
Liveness properties - None defined (may not be needed)
Constant bounds - MaxValue = 10 (reasonable)
Symmetry - Not applicable for this spec
State constraints - Not needed (small state space)

─────────────────────────────────────────────────────────
5. RECOMMENDATIONS
─────────────────────────────────────────────────────────

-> Run: /tla-check for exhaustive verification
-> Consider adding liveness properties if termination matters

═══════════════════════════════════════════════════════════
REVIEW COMPLETE
═══════════════════════════════════════════════════════════