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 agentmods add skills/tlaplus/agentskills/tlaplus-from-sourcenpx skills add tlaplus/AgentSkills --skill tlaplus-from-sourcegit clone --depth 1 https://github.com/tlaplus/AgentSkillsWhat 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 | $0.00079 | $0.02950 |
| Opus 5 | $0.00039 | $0.01475 |
| Sonnet 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 3d 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.
- 3d 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 (36 stars, last pushed 7mo ago), licensed MIT. It adds 79 tokens to every session and 2,950 once invoked, about $0.0004 per session on Opus 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
instrument-data-to-allotrope
Convert laboratory instrument output files (PDF, CSV, Excel, TXT) to Allotrope Simple Model (ASM) JSON format or flattened 2D CSV. Use this skill when scientists need to standardize instrument data for LIMS systems, data lakes, or downstream analysis. Supports auto-detection of instrument types. Outputs include full…
exploratory-data-analysis
Perform bounded, local exploratory analysis of explicitly supported scientific files. Use for redacted CSV/TSV/JSON profiles; optional NumPy, HDF5, FASTA/FASTQ, and basic image metadata inspection; missingness/leakage audits; outlier and transformation sensitivity; and rigorous EDA report scaffolds. Other domain…
mapping-to-snomed
Maps clinical concept spans extracted by OpenMed to SNOMED CT concepts through a USER-SUPPLIED terminology server (the user's own Ontoserver, Snowstorm, or UMLS/UTS), never a bundled vocabulary. Use when the user wants to code findings, disorders, procedures, body structures, or substances to SNOMED CT, run an ECL…
auditing-subgroup-fairness
Audit an OpenMed NER or de-identification model for performance disparities across demographic subgroups (sex, age band, race/ethnicity when available) using openmed.eval.fairnessreport. Use when the user wants per-subgroup recall and leakage, wants to check whether de-identification under-protects a group, wants to…
overleaf-sync
Two-way sync between a local paper directory and an Overleaf project, so ARIS audit/edit workflows stay on the local copy while collaborators edit in the Overleaf web UI. Use when user says "同步 overleaf", "overleaf sync", "推送到 overleaf", "connect overleaf", "Overleaf 桥接", "pull overleaf", "push overleaf", or wants to…
mixed-precision
Use FP16/BF16 mixed precision to accelerate training and reduce memory. Use when optimizing GPU performance.