program-to-tlaplus-spec-generator

Automatically generate TLA+ specifications from program code, repositories, or system implementations. Use when asked to generate TLA+ spec, create TLA+ specification from code, convert program to TLA+, formalize system in TLA+, extract TLA+ model from code, or when working with formal specification of concurrent systems, distributed systems, protocols, algorithms, or state machines that need to be verified.

Install with Tessl CLI

npx tessl i github:ArabelaTso/Skills-4-SE --skill program-to-tlaplus-spec-generator

What are skills?

Review — 85%

Does it follow best practices?

If you maintain this skill, you can automatically optimize it using the tessl CLI to improve its score:

npx tessl skill review --optimize ./path/to/skill

Learn more

Validation — 11 / 11 Passed

Validation for skill structure

SKILL.md

Review

Evals

Evaluation results

100%

Formal Specification of a Rate Limiter

TLA+ module structural elements

Criteria

Without context

With context

Module header/footer

100%

EXTENDS clause

100%

vars tuple

100%

UNCHANGED in actions

100%

Separate action definitions

100%

Next with disjunction

100%

Spec with stuttering

100%

TypeInvariant defined

100%

Bounded tokens variable

100%

Lock modeled as boolean

100%

Safety property present

100%

Without context: $0.3356 · 2m 51s · 11 turns · 15 in / 7,688 out tokens

With context: $0.6764 · 3m 36s · 23 turns · 1,716 in / 8,626 out tokens

87%

-5%

Document the Formal Model of a Concurrent Queue

Program-to-spec mapping documentation

Criteria

Without context

With context

State variable mapping table

100%

Action mapping table

100%

Abstractions section

100%

Assumptions section

100%

37%

Verification guidance present

100%

Model parameters suggested

100%

TLC config or INVARIANTS hint

100%

Queue modeled as Seq

100%

Lock modeled explicitly

Bounded queue size constraint

100%

Objects modeled as records

100%

Wait/notify abstracted

100%

Without context: $0.5926 · 4m 24s · 16 turns · 21 in / 12,707 out tokens

With context: $0.7271 · 4m 16s · 23 turns · 189 in / 12,008 out tokens

100%

10%

Formal Specification of a Go Pipeline Worker Pool

Go language TLA+ patterns

Criteria

Without context

With context

Channels modeled as Seq

100%

Workers modeled as processes

100%

Select modeled as disjunction

100%

Channel capacity bounded

100%

Done/shutdown state modeled

100%

Receive uses Head/Tail

100%

Send uses Append

100%

process() abstracted

100%

Slices/lists use Seq type

75%

100%

EXTENDS Sequences

100%

WaitGroup abstracted

100%

Without context: $0.6906 · 4m 42s · 17 turns · 23 in / 15,766 out tokens

With context: $1.2384 · 6m 12s · 27 turns · 6,126 in / 21,634 out tokens

Evaluated: about 12 hours ago
Agent: Claude Code

Table of Contents

Formal Specification of a Rate Limiter Document the Formal Model of a Concurrent Queue Formal Specification of a Go Pipeline Worker Pool

Is this your skill?

If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.