Individual skill

requirement-to-tlaplus-property-generator

Automatically derives TLA+ properties (invariants, safety, liveness) from natural-language requirements or structured requirement documents. Resolves ambiguities, asks clarifying questions for underspecified requirements, and outputs TLA+-compatible property definitions with semantic explanations. Use when translating system requirements, specifications, or behavioral constraints into formal TLA+ temporal logic properties for verification with TLC model checker.

skills/requirement-to-tlaplus-property-generator/SKILL.md

Read pinned source

Source commit 4f38503747e0617504bce5329283ef837d375c09

What was checked

Matches the observed repository HEAD: Yes
Scanner rules are current: No
Repository scan complete: No
Skill scan complete: Yes
Observed behavior: Not checked yet
Last checked: Nov 6, 2026

These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.

Install this skill

Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.

An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.

Repository context

Repository stars (not skill ratings): 260
Repository last updated: Aug 21, 2026
License: Apache-2.0

Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.

claude-skills Repository topic
metaprogramming Repository topic
software-development Repository topic
software-engineering Repository topic
claude Repository topic
claude-code Repository topic
engineering Derived category

Files and excerpt

File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.

Browse files

SKILL.mdcore · 7,619 bytes
references/clarification_patterns.mddoc · 10,441 bytes
references/requirement_patterns.mddoc · 8,838 bytes
references/tlaplus_syntax.mddoc · 7,428 bytes

Read excerpt


# Requirement to TLA+ Property Generator

## Overview

This skill transforms natural-language requirements into formal TLA+ properties, enabling rigorous verification of system specifications. It handles invariants, safety properties, and liveness properties, resolving ambiguities and seeking clarification when needed.

## Workflow

### Step 1: Analyze the Requirement

Parse and understand the input requirement:

1. **Identify requirement type**:
   - Invariant: "The system always maintains property P"