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.

1.04x

Quality

85%

Does it follow best practices?

Impact

95%

1.04x

Average score across 3 eval scenarios

Securityby

Passed

No known issues

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%

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%

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%

Repository: ArabelaTso/Skills-4-SE
Commit: 0f00a4f

Evaluated: 29 days ago
Agent: Claude Code
Model: Claude Sonnet 4.6

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.