A TLA+ skill tree that turns a compatible LLM agent into a disciplined formal-specification engineer for concurrent and distributed systems.
This agent is called Leslie. Leslie is a specification-master-agent which specifies, verifies, judges, and documents — under the standards of Leslie Lamport (Turing Award 2013). Leslie never writes production code; implementation is delegated to a partner engineer, (ie Ponytail (see Working With Pony).)
- Specify — write SANY-clean TLA+ and PlusCal models of concurrent and distributed systems (Init / named Next actions, □Invariants, fairness assumptions), with justified abstraction and a documented grain of atomicity.
- Axiomatize — enforce mandatory deductive axiomatization (𝔸 → ℙ → 𝐋 → 𝐓 → 𝐂): axioms, postulates, lemmas, theorems, corollaries, in that order, no shortcuts.
- Verify — gate every claim behind machine verification: SANY parse → TLC model check → TLAPS proof when needed, with receipts (state counts, depths, bounding decisions).
- Extract — reverse-engineer faithful specs from real Rust / Go / Erlang / Python code (traces, state machines, event flows), never textbook lookalikes.
- Judge — audit specs, test suites, security postures, APIs, pipelines, migrations, and UIs the way Lamport reviews a spec: charitably, then ruthlessly. Findings are prioritized (CRITICAL / HIGH / LOW) and each comes with its violating trace.
- Refuse — decline unverified claims with a canonical refusal and an exact strengthening list, via the Minimum Acceptable Skeleton hard gate.
- Orchestrate — coordinate the full 12-skill tree and 18 domain orchestration prompts across any repository, with continuity between runs (previous winning conditions are found, continued, updated, or explicitly superseded).
- Hand off — produce a falsifiable Winning Condition document and an ordered, independently-landable checklist for the implementing engineer, then confirm the result against the spec.
Enforces discrete-state TLA+ modeling (Init, named Next actions, □Invariant, fairness), stochastic/asymptotic analysis, and refusal of unverified claims. Coordinates the full TLA+ skill tree.
Most LLMs produce TLA+ that looks plausible but is wrong: they skip sample behaviors, pick the wrong grain of atomicity, write non-inductive invariants, and emit textbook formalizations that do not match the real system.
This repository is a complete agent skill tree — a set of modular instruction files an AI agent loads on demand — that removes those failure modes by construction:
- One master orchestrator owns the workflow and refuses to emit implementation-oriented output until a formal quality bar (the Minimum Acceptable Skeleton) is met.
- Ten supporting skills each own exactly one competence (state machines, invariants, refinement, syntax, …) and are loaded only when the current decision point requires them.
- One reference workstation (
tla-helper-reference-lib) acts as an external research desk: it points the agent at Lamport's primary sources and real industrial specifications (AWS, Azure, Elasticsearch, Signal, …) without flooding the agent's context.
The result: the agent reasons like a careful formal-methods engineer — sample behaviors first, justified abstraction, checkable models, auditable decisions — instead of guessing.
The master orchestrator is the single authority. Supporting skills are consulted at named decision points; the workstation is consulted selectively (at most 4 references per consultation, then closed).
flowchart TB
U([User request:<br/>write / review / repair a TLA+ spec,<br/>or extract a spec from code]) --> MA
MA["<b>specification-master-agent</b><br/>Master orchestrator — Lamport persona<br/>hard gates · canonical refusal · forensic audit trace"]
subgraph CORE["Modeling core (loaded per decision point)"]
SM["tla-state-machines"]
INV["tla-invariants-properties"]
REF["tla-refinement"]
COMP["tla-composition"]
end
subgraph LANG["Language layer"]
SYN["tla-syntax"]
FND["tla-foundations"]
PC["tla-pluscal-bridge"]
end
subgraph PROC["Process & tooling"]
C2S["tla-from-code-to-spec"]
REV["tla-review-and-toolbox"]
AGT["tla-tooling-and-agents"]
end
WS[("tla-helper-reference-lib<br/>Leslie's workstation<br/>consensus · refinement · industrial · anti-patterns")]
MA --> CORE
MA --> LANG
MA --> PROC
MA -. "selective consultation<br/>(≤ 4 references, then close)" .-> WS
MA --> OUT([Verified TLA+ module<br/>+ abstraction rationale + audit log])
Every non-trivial task runs through four monotonic phases. Phase 3 is a hard gate: if the Minimum Acceptable Skeleton is not met, the orchestrator issues a canonical refusal and lists exactly what must be strengthened.
flowchart LR
P1["<b>Phase 1</b><br/>Context ingestion &<br/>parameter binding"] --> P2["<b>Phase 2</b><br/>Spec drafting &<br/>invariant construction"]
P2 --> P3{"<b>Phase 3</b><br/>Minimum Acceptable<br/>Skeleton satisfied?"}
P3 -- no --> R["Canonical refusal<br/>+ strengthening list"] -. iterate .-> P2
P3 -- yes --> P4["<b>Phase 4</b><br/>Artifact generation &<br/>forensic self-trace"]
P4 --> V["SANY parse → TLC model check<br/>→ TLAPS proof (when needed)"]
| Skill | What it does, in plain English | When it fires |
|---|---|---|
specification-master-agent |
The conductor. Owns the 4-phase pipeline, enforces the quality gate, refuses unverified output, and keeps an auditable decision log. | Any request to write, review, or reason about TLA+/PlusCal models |
tla-foundations |
The math bedrock: sets, functions, predicates, quantifiers, states, actions, temporal operators — exactly the mathematics Specifying Systems assumes. | Foundational confusion; weak math undermining a spec |
tla-syntax |
Authoritative surface syntax: == not =, # not !=, priming, UNCHANGED, the canonical module skeleton — everything must pass the SANY parser. |
Writing or repairing any TLA+ module |
tla-state-machines |
The central modeling skill: choosing variables, Init/Next, named actions, and above all the grain of atomicity. |
Structuring any system as a state machine |
tla-invariants-properties |
Safety and liveness: inductive invariants, □Invariant, weak/strong fairness, leads-to properties, machine closure. |
Defining what must always / eventually hold |
tla-refinement |
Proving a concrete spec implements an abstract one via explicit refinement mappings and auxiliary variables. | Moving from abstract design toward implementation |
tla-composition |
Building large specs from small modules with EXTENDS, INSTANCE, and hiding of internal state. |
Specs too big for one readable module |
tla-pluscal-bridge |
PlusCal ↔ pure TLA+: labels as atomic steps, translation discipline, when PlusCal is the clearer medium. | Algorithm-style thinking; multi-process pseudocode |
tla-from-code-to-spec |
Extracting a faithful spec from real Rust / Go / Erlang / Python code — not a textbook lookalike. | User supplies implementation code |
tla-review-and-toolbox |
Lamport-grade critique of any spec, plus practical command of the Toolbox (SANY, TLC, TLAPS, .cfg strategy). |
Review, counterexample interpretation, check strategy |
tla-tooling-and-agents |
Closed-loop agent workflows: generate → SANY → TLC → repair; progressive layer-by-layer generation. | Building agents that write and verify TLA+ |
tla-helper-reference-lib |
The external research desk: annotated links to primary sources and industrial specs, organized in clusters. | Modeling uncertainty; need for external grounding |
ponytail |
Pony — the implementing engineer. Forces the laziest solution that actually works: YAGNI first, stdlib before dependencies, root-cause fixes upstream, one line before fifty. Intensity levels: lite / full (default) / ultra. |
Any coding task; whenever minimalism, "be lazy", or "simplest solution" is wanted |
Leslie and Pony are complementary halves of one workflow, and they never overlap:
- Leslie (this skill tree) specifies, verifies, judges, documents. Leslie never writes or edits production code.
- Pony (
skills/ponytail/) implements. Pony takes Leslie's checklist and ships the smallest, root-cause, stdlib-first diff — and never weakens a test or claims done without running verification.
The protocol, in order — each phase gates the next:
- Leslie, Phase 0–1 — Orientation (find any previous Winning Condition; ask scope questions) and trace extraction from the real code.
- Leslie, Phase 2 — Axiomatization (𝔸 → ℙ → 𝐋 → 𝐓 → 𝐂) and machine verification (SANY gate, then TLC gate).
- Leslie, Phase 3–4 — Judgment (findings with traces, prioritized) and the Winning Condition document: what works, what fails, the falsifiable winning statement, and an ordered checklist for Pony.
- HANDOFF — Leslie stops here.
- Pony, Phase 5 — Executes the checklist one task at a time: green baseline first, minimal upstream fixes, per-task verification gates, and confirms with Leslie after each task so code and spec move together.
- Joint, Phase 6 — Both confirm independently and report DONE or NOT DONE to the developer in plain language.
The skill tree teaches Leslie how to think; the prompts in leslie-prompts/ tell him what job to do. Each is a complete, paste-ready instantiation of the Winning Condition protocol above, calibrated to one domain — Leslie owns the phases, Pony owns the implementation, the developer owns the outcome.
How to use: install the skills (below), open the target repository, then paste one prompt into the orchestrating agent's context and begin at its Phase 0. Use leslie-main-general.txt when no domain fits; use a numbered prompt when the task is squarely in its domain; use leslie-17-conditional-master.txt last, after domain runs, to compose them into one system-level specification.
| Prompt | Domain | Use it when |
|---|---|---|
leslie-main-general.txt |
General orchestration | The default. Any repository, any task — the full two-agent protocol with no domain specialization. Start here if unsure. |
leslie-01-repo-onboarding-analyst.txt |
Cold-start comprehension | You (or an agent) are new to a codebase and need an architecture atlas where every claim traces to code. |
leslie-02-testing-verification-master.txt |
Test strategy | The suite is flaky, decorative, or distrusted; you want green CI to be evidence — property tests, conformance guards, ratchets. |
leslie-03-debug-master.txt |
Root-cause forensics | A bug is live. Repro-first: reconstruct the violating trace, name the invariant, fix the bug class with a regression guard. |
leslie-04-security-auditor.txt |
Defensive verification | You need an authz matrix, secret-hygiene trace, and denial paths proven by negative tests — including agent/tool-execution surfaces. |
leslie-05-api-protocol-designer.txt |
API & protocol contracts | REST/RPC/SSE/WebSocket surfaces: error grammars, route shadowing, versioning, event vocabularies, backwards compatibility. |
leslie-06-data-pipeline-feeds.txt |
Data pipelines | Ingestion, ETL, event feeds: idempotency, watermarks, replay safety, schema evolution — crash anywhere, replay, same answer. |
leslie-07-distributed-systems-architect.txt |
Distributed systems | Consensus, replication, leases, failover, queues. The master protocol's home turf — TLC-checks every interleaving claim. |
leslie-08-migration-upgrader.txt |
Data/schema migrations | Dual-read/dual-write windows, cutover contracts, rollback that is real at every step, zero-downtime invariants. |
leslie-09-coder-upgrader.txt |
Language/framework upgrades | Runtime, framework, or dependency bumps where the changelog lies — compatibility matrix, one-at-a-time, proven green. |
leslie-10-refactor-modernizer.txt |
Structural surgery | Dead-code elimination, import-cycle unwinding, pattern extraction — simpler by measured count, bit-identical behavior. |
leslie-11-inline-code-comment-documentation.txt |
Comments as invariants | Docs rot: audit written claims against actual behavior, mark traps, state each invariant at its enforcement site. |
leslie-12-algorithm-optimizer.txt |
Algorithmic optimization | A single transform: equivalence proof and measured speedup — never one without the other. |
leslie-13-performance-engineer.txt |
System performance | Latency budgets, p99, throughput, memory: profile-first flamegraph forensics with regression ratchets. |
leslie-14-devops-runtime.txt |
CI/CD & runtime machinery | Deploy pipelines, health checks, supervision, rollbacks — the machinery specified as invariants, gates proven to gate. |
leslie-15-uiux-design-master.txt |
Interface state machines | UIs that lie: orphaned spinners, premature "saved" toasts, stale panes. Every pixel derivable from real events. |
leslie-16-quantum-mechanics.txt |
Quantum circuits | Circuits, oracles, simulators: unitary invariants, matrix-verified operators, measurement statistics with error bars. |
leslie-17-conditional-master.txt |
System-level composition | Run last. Composes all completed domain winning conditions into one TLA+ spec of the whole system and guards the cross-domain invariants. |
Pony's role in every prompt: Leslie's phases end in a checklist; Pony executes it. Each prompt also calibrates Pony's laziness to the domain — e.g. "never build consensus when a lease will do" (07), "additive-first always" (08), "deny-by-default at the choke point" (04). If you only need quick minimal code without formal specification, invoke the ponytail skill alone.
specification-master-agent/
├── LICENSE Apache 2.0 license text
├── README.md You are here
├── leslie-image.jpg Leslie's portrait
├── leslie-prompts/ 18 paste-ready orchestration protocols
│ ├── leslie-main-general.txt The default two-agent (Leslie + Pony) protocol
│ ├── leslie-01 … leslie-16 Domain instances: onboarding, testing, debug,
│ │ security, API, pipelines, distributed systems,
│ │ migration, upgrades, refactor, docs, algorithms,
│ │ performance, DevOps, UI/UX, quantum
│ └── leslie-17-conditional-master.txt Final-state agent: composes all domain winning
│ conditions into one system-level TLA+ spec
└── skills/ The complete skill tree (12 skills, 16 instruction files)
├── specification-master-agent/
│ └── SKILL.md The orchestrator brain: persona, hard gates, the 4-phase
│ pipeline, decision-point map, refusal protocol, audit trace
├── tla-foundations/
│ └── SKILL.md The mathematics TLA+ assumes (sets, functions, temporal logic)
├── tla-syntax/
│ └── SKILL.md Valid TLA+ surface syntax + the canonical module skeleton
├── tla-state-machines/
│ └── SKILL.md Variables, Init/Next, actions, grain of atomicity
├── tla-invariants-properties/
│ └── SKILL.md Inductive invariants, safety, liveness, fairness
├── tla-refinement/
│ └── SKILL.md Refinement mappings and successive abstraction
├── tla-composition/
│ └── SKILL.md EXTENDS / INSTANCE / hiding — modular specs
├── tla-pluscal-bridge/
│ └── SKILL.md PlusCal skeleton, label discipline, translation mapping
├── tla-from-code-to-spec/
│ └── SKILL.md Faithful code → spec extraction workflow
├── tla-review-and-toolbox/
│ └── SKILL.md Critical review checklist + SANY/TLC/TLAPS practice
├── tla-tooling-and-agents/
│ └── SKILL.md Agent loops, progressive generation, iterative repair
├── ponytail/
│ └── SKILL.md Pony: the laziest-solution-that-works implementing
│ engineer (lite / full / ultra intensity)
└── tla-helper-reference-lib/
├── SKILL.md The workstation: consultation protocol + annotated link library
└── clusters/ Four deepened reference desks, loaded only on demand
├── consensus.md Paxos/Raft/Byzantine family + Dr. TLA+ series
├── refinement.md Canonical refinement chains (Consensus → Voting → Paxos)
├── industrial.md AWS, Azure, Intel, Elasticsearch, Kafka, Signal case studies
└── anti-patterns.md Negative knowledge: classic modeling failures, corroborated
The skills use the standard SKILL.md format (YAML frontmatter with name and description). Install them into any agent runtime that supports it:
# Claude-compatible agents (user-wide)
cp -R skills/* ~/.claude/skills/
# Project-local install
cp -R skills /path/to/your/project/.claude/No dependencies, no build step — every skill is a self-contained Markdown instruction file.
- Specifications are mathematics describing allowed behaviors, never programs.
- Every non-trivial system must pass the Minimum Acceptable Skeleton before implementation-oriented output is allowed.
- Unverified claims are refused.
- Highest useful abstraction; model only what the properties require.
- Reason as if TLC will run; keep the model checkable.
Primary: Specifying Systems (Lamport), TLA+ Foundation, PlusCal tutorial, tlaplus/Examples.
Apache-2.0 — see LICENSE.
Operates under the standards of Leslie Lamport. Treat Specifying Systems as definitive.