Agent-Skills.md

Agent Skills: TLA+ Generator

Generate and analyze TLA+ specifications for distributed systems verification

distributed-systemsID: a5c-ai/babysitter/tla-plus-generator

Repository

a5c-ai/babysitter
a5c-aiLicense: MIT
244

Install this agent skill to your local

pnpm dlx add-skill https://github.com/a5c-ai/babysitter/tree/HEAD/plugins/babysitter/skills/babysit/process/specializations/domains/science/computer-science/skills/tla-plus-generator

Skill Files

Browse the full folder contents for tla-plus-generator.

Download Skill

Loading file tree…

plugins/babysitter/skills/babysit/process/specializations/domains/science/computer-science/skills/tla-plus-generator/SKILL.md

Skill Metadata

Name
tla-plus-generator
Description
Generate and analyze TLA+ specifications for distributed systems verification

TLA+ Generator

Purpose

Provides expert guidance on generating TLA+ specifications for distributed systems design and verification.

Capabilities

  • TLA+ module generation from protocol description
  • Invariant and temporal property specification
  • State space exploration configuration
  • PlusCal to TLA+ translation
  • Model checking execution
  • Refinement mapping

Usage Guidelines

  1. System Modeling: Model system components and state
  2. Action Specification: Define system actions/transitions
  3. Property Specification: Specify safety and liveness properties
  4. Model Checking: Configure and run TLC model checker
  5. Refinement: Relate abstract and concrete specifications

Tools/Libraries

  • TLA+ Toolbox
  • TLC model checker
  • TLAPS proof system
  • PlusCal