Getting it into your agent
One page per mod, every tool's command on it. A separate URL per tool would split the same page into five that compete with each other.
npx skills add tlaplus/AgentSkills --skill tlaplus-from-sourcegit clone --depth 1 https://github.com/tlaplus/AgentSkillsWrote this? Show the measurements
A badge with what this costs and how it scanned, read live from this page, so it follows the numbers instead of freezing them. Markdown for a README, HTML for a documentation site or a project page.
[](https://agentmods.dev/skills/tlaplus/agentskills/tlaplus-from-source)<a href="https://agentmods.dev/skills/tlaplus/agentskills/tlaplus-from-source"><img src="https://agentmods.dev/badge/skills/tlaplus/agentskills/tlaplus-from-source/github.svg" alt="Measured on agentmods" height="20"></a>Or the 80×15 button, for a site that already has a row of RSS and ATOM ones. Only the verdict fits; the numbers stay here.
<a href="https://agentmods.dev/skills/tlaplus/agentskills/tlaplus-from-source"><img src="https://agentmods.dev/badge/skills/tlaplus/agentskills/tlaplus-from-source.svg" alt="Reviewed on agentmods" width="80" height="20"></a>What it costs to keep this loaded
Counted locally with the o200k_base tokenizer, which is exact for GPT models; Claude uses its own tokenizer and its counts differ. Treat this as one consistent yardstick across the catalogue rather than a bill. Prices are per million input tokens.
| Model | Per session | Once invoked |
|---|---|---|
| Fable 5.1 | $0.00079 | $0.02950 |
| Opus 5.5 | $0.00032 | $0.01180 |
| Sonnet 5.5 | $0.00016 | $0.00590 |
| Haiku 4.5 | $0.00008 | $0.00295 |
Grade A, and why
tlaplus-from-source scanned grade A with 0 findings against 26 rules in 11 categories — prompt injection, anti-refusal, data exfiltration, privilege escalation, supply chain, agent snooping, system-prompt leakage, SSRF and excessive agency — measured 1mo ago.
A static scan of the body, not an audit. Every finding is printed with the line that produced it so you can judge whether it matters here. A mod is markdown that instructs an agent; that is exactly why what it instructs is worth reading.
Nothing flagged
None of the 26 patterns this scan looks for appear in this file: no shell pipes, no recursive deletes, no credential paths, no hidden text, no instruction-override or anti-refusal phrasing, no agent-config snooping. That is not a guarantee, it is the absence of the things that are checkable.
How it starts
The opening of the file, as written. The whole thing — 413 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Generate High-Level TLA+ Model from Source Code
Create a TLA+ specification from source code by understanding the code's intent, abstracting implementation details, and focusing on the essential concurrent/distributed behavior.
Philosophy
TLA+ models should capture what the system does, not how it does it:
- Focus on state transitions and their effects
- Abstract away implementation details (memory management, error handling boilerplate)
- Identify the core concurrent/distributed behavior worth verifying
- Keep the model small enough to be tractable for model checking
Workflow Overview
┌─────────────────────────────────────────────────────────────────┐
│ Phase 1: Understand the Code │
│ → What problem does it solve? │
│ → What are the key functions and their purposes? │
│ → What state is being managed? │
└─────────────────────────────────────────────────────────────────┘
↓
┌─────────────────────────────────────────────────────────────────┐
│ Phase 2: Identify Abstractions │
│ → What are the essential state variables? │
│ → What are the atomic actions? │
│ → What concurrency/ordering matters? │
└─────────────────────────────────────────────────────────────────┘
↓
┌─────────────────────────────────────────────────────────────────┐
│ Phase 3: Write TLA+ Specification │
│ → Define constants and variables │
│ → Write Init and actions │
│ → Define Next as disjunction of actions │
│ → Check specification syntax with TLC parser SANY │
└─────────────────────────────────────────────────────────────────┘
↓
┌─────────────────────────────────────────────────────────────────┐
│ Phase 4: Propose Properties │
│ → Safety invariants │
│ → Safety properties (what must be true at all times) │
│ → Liveness properties (what must eventually happen) │
└─────────────────────────────────────────────────────────────────┘
What this file has done since we first saw it
Hashed on every crawl. A supply-chain change to an agent config is a question of when, not whether, so the history is kept rather than the latest state alone.
- 1mo ago First seen · 413 lines · 79 tokens per session scan A b097f1016742
tlaplus-from-source is a skill published in the GitHub repository tlaplus/AgentSkills (42 stars, last pushed 8mo ago), licensed MIT. It adds 79 tokens to every session and 2,950 once invoked, about $0.0003 per session on Opus 5.5. A static security scan graded it A with 0 findings. No closer match exists in the catalogue, so it is treated as the original; first seen 2026-08-30.
Other skills, from other repositories
trace
Evidence-driven tracing lane that orchestrates competing tracer hypotheses in Claude built-in team mode.
pos-tagging-fixes
Diagnose and fix part-of-speech tagging in the compromise source repository. Choose between lexical data, ambiguity clues, indexed neighbour rules, preTagger logic, and postTagger patterns with attention to execution order, side effects, runtime, and bundle size. Use for internal tagging changes, not ordinary…
smiles-validation
Strict SMILES validation, structural comparison, and modification verification. Catches invalid LLM-generated molecules.
linear-solvers
Select and configure linear solvers for systems Ax=b in dense and sparse problems. Use when choosing direct vs iterative methods, diagnosing convergence issues, estimating conditioning, selecting preconditioners, or debugging stagnation in GMRES/CG/BiCGSTAB.
nonlinear-solvers
Select and configure nonlinear solvers for f(x)=0 or min F(x). Use for Newton methods, quasi-Newton (BFGS, L-BFGS), Broyden, Anderson acceleration, diagnosing convergence issues, choosing line search vs trust region, and analyzing Jacobian quality.
numerical-stability
Analyze and enforce numerical stability for time-dependent PDE simulations. Use when selecting time steps, choosing explicit/implicit schemes, diagnosing numerical blow-up, checking CFL/Fourier criteria, von Neumann analysis, matrix conditioning, or detecting stiffness in advection/diffusion/reaction problems.