# Photoszzt Tlaplus AI Tools Tla Model Checking

> TLA+ Model Checking Workflow

- Skill: `tomevault-io/photoszzt-tlaplus-ai-tools-tla-model-checking` (Agent Skill, multi-file: 2 files)
- Install (CLI): `npx skillmds@latest add tomevault-io/photoszzt-tlaplus-ai-tools-tla-model-checking`
- Raw SKILL.md: https://api.skillmd.com/api/skills/tomevault-io/photoszzt-tlaplus-ai-tools-tla-model-checking/raw
- Safety review: pending (external: skill-scanner PASS, skillspector PASS)
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: AI & ML
- Author: tomevault-io (https://skillmd.com/u/tomevault-io)
- Updated: 2026-09-17
- Page: https://skillmd.com/skills/tomevault-io/photoszzt-tlaplus-ai-tools-tla-model-checking

---


# TLA+ Model Checking Workflow

Orchestrate the full model checking workflow: parse, configure, smoke test, and exhaustive check.

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

**Reference**: For detailed educational content on TLC configuration syntax, performance tuning, debugging, and best practices, read `skills/tla-model-checking/reference.md` on demand.

## Usage

```
/tla-model-checking @Counter.tla
/tla-model-checking specs/MySpec.tla
```

Both forms work identically. See `skills/shared/path-normalization.md` for path normalization rules.

## Implementation

**Step 1: Validate Argument**

If no spec file path argument is provided, print `Error: No file path provided. Usage: /tla-model-checking <path.tla>` and stop.

Strip any leading `@` from the argument to get `SPEC_PATH`. Print `Spec: <SPEC_PATH>`.

**Step 2: Parse with SANY**

Read the file first to confirm it exists and ends with `.tla`.

Call `mcp__plugin_tlaplus_tlaplus__tlaplus_mcp_sany_parse` with `fileName` set to `SPEC_PATH`.

- If parsing fails: print the errors to the user and **stop**. Do not proceed.
- If parsing succeeds: print `Parse: OK` and continue.

**Step 3: Apply CFG Selection Algorithm**

Apply the CFG Selection Algorithm documented in `skills/shared/cfg-selection-algorithm.md`.

Store the final cfg path in `FINAL_CFG`.

**Step 4: Smoke Test**

Call `mcp__plugin_tlaplus_tlaplus__tlaplus_mcp_tlc_smoke` with:

- `fileName` set to `SPEC_PATH`
- `cfgFile` set to `FINAL_CFG`
- `seconds` set to `3`

- If violations found: report them to the user and ask "Smoke test found violations. Would you like to proceed to full model check anyway, or fix the issues first?"
- If no violations: print `Smoke test: Passed` and continue.

**Step 5: Full Model Check**

Call `mcp__plugin_tlaplus_tlaplus__tlaplus_mcp_tlc_check` with:

- `fileName` set to `SPEC_PATH`
- `cfgFile` set to `FINAL_CFG`

Report: total states explored, distinct states, diameter, any violations (include full counterexample traces), and final result (pass/fail).

If TLC reports OutOfMemoryError or runs excessively long, suggest reducing constant values, adding state constraints, or using `/tla-smoke` for quick feedback.

**Step 6: Report Results**

Summarize the full workflow:

```
Model Checking Summary for <SPEC_PATH>
  Parse:      OK
  Config:     <CFG_PATH>
  Smoke test: <passed/violations found>
  Full check: <passed/violations found>

  States explored: <N>
  Distinct states: <N>
```

If violations were found, suggest: "Use `/tla-debug-violations` or the trace-analyzer agent to understand the counterexample."

If all passed, suggest: "Consider increasing constant values or adding more properties to strengthen verification."

---
> Source: [photoszzt/tlaplus-ai-tools](https://github.com/photoszzt/tlaplus-ai-tools) — distributed by [TomeVault](https://tomevault.io).
<!-- tomevault:4.0:skill_md:2026-06-03 -->