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 younes-io/agent-skills --skill tla-proofgit clone --depth 1 https://github.com/younes-io/agent-skillsWrote 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/younes-io/agent-skills/tla-proof)<a href="https://agentmods.dev/skills/younes-io/agent-skills/tla-proof"><img src="https://agentmods.dev/badge/skills/younes-io/agent-skills/tla-proof/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/younes-io/agent-skills/tla-proof"><img src="https://agentmods.dev/badge/skills/younes-io/agent-skills/tla-proof.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.00087 | $0.00991 |
| Opus 5 | $0.00044 | $0.00495 |
| Sonnet 5 | $0.00017 | $0.00198 |
| Haiku 4.5 | $0.00009 | $0.00099 |
Grade A, and why
tla-proof 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 11d 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 — 108 lines — stays where its author put it; the contents beside it link to each section on GitHub.
TLA+ Proof
Outputs
- Updated proof-bearing TLA+ module(s):
*.tla - TLAPS run artifacts:
.tla-proof/runs/<run-id>/...
Non-Negotiables (Honesty Rules)
- Never claim full system correctness from a partial proof.
- Always report what was proved, what failed, and what was omitted.
- Always surface trust boundaries (
ASSUME,AXIOM, omitted proofs, imported facts). - Never conflate TLC outcomes with TLAPS outcomes; treat them as different evidence.
- Always keep theorem statements stable while debugging unless the user approves spec changes.
Workflow (Target Class -> Proof Plan -> TLAPS -> Iterate)
1) Pin Down Target and Trust Boundary
Record:
- theorem statement(s) in scope
- proof class: direct fact, inductive invariant, refinement, formula equivalence, safety, liveness
- assumptions/environment model
- required imported definitions/lemmas
- candidate strengthening invariants or helper lemmas if the target does not look inductive yet
- proof granularity target (quick progress vs fully structured proof)
If theorem intent is ambiguous, state candidate interpretations and choose one explicitly.
If the user is refactoring a spec and wants semantic preservation, consider a direct equivalence theorem (F <=> G) instead of only bounded TLC evidence.
2) Draft Minimal Hierarchical Proof Structure
Start with the smallest stable structure:
THEOREM ...PROOFSUFFICES,HAVE,CASE,PICK,TAKE,WITNESS,QEDas needed
Prefer explicit sub-lemmas over long single-step BY clauses.
Use BY DEF ... only for required definitions.
Formula-equivalence proofs for refactors are a supported pattern, for example THEOREM F <=> G BY DEF F, G.
Match the structure to the proof class:
- inductive invariant/safety: isolate base case vs step case and split
Nextby action - refinement: state the abstraction relation/refinement mapping and prove init/step obligations separately
- formula equivalence: start with
THEOREM F <=> G; if a one-line proof fails, split intoF => GandG => F - liveness/starvation freedom: pin down fairness and ranking assumptions before proof search, then expect auxiliary lemmas
What ships with it
8 files beside SKILL.md in the same directory: the scripts, references and assets a skill reads on demand. Not counted in the per-session cost; read them before you install if any of them is executable.
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.
- 11d ago First seen · 108 lines · 87 tokens per session scan A af795582da26
tla-proof is a skill published in the GitHub repository younes-io/agent-skills (20 stars, last pushed 2mo ago), licensed MIT. It adds 87 tokens to every session and 991 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
automatic-differentiation-advanced
Extend Sounio's automatic differentiation capabilities to higher‑order derivatives, Hessians, differentiation through control flow, and GPU‑accelerated gradient computation, enabling state‑of‑the‑art scientific machine learning.
epistemic-uncertainty-quantification
Extend Sounio's epistemic types with advanced uncertainty quantification methods, such as confidence intervals, non‑Gaussian distributions, and Dempster‑Shafer evidence combination, positioning the language at the state‑of‑the‑art in measurement science.
formal-verification-epistemic
Integrate formal verification tools (SMT solvers, Lean) to prove properties of epistemic programs, such as uncertainty bounds, confidence guarantees, and provenance integrity, establishing Sounio as a language with mathematically verified scientific claims.
lean-axiom-provenance
Find out what a Lean 4 project actually rests on, and why. Reports every theorem reaching a sorry anywhere upstream, everything settled by nativedecide rather than the kernel, and the shortest path from any declaration to any axiom with each hop labelled a statement dependency or a proof dependency. Use when the user…
lean-generated-proof-audit
Check whether a machine-generated Lean 4 proof actually proves its theorem. A proof can appear in the environment, pass lake build, and still not have been proved: when elaboration fails Lean admits the declaration carrying sorryAx, which an axiom report cannot tell apart from a sorry somebody typed. Use when auditing…
sounio-epistemic-types
Work on Sounio epistemic computing: Knowledge/uncertainty/confidence/provenance, ontology bindings, and dependent epistemic subtyping/proofs; use when editing compiler/src/epistemic/, compiler/src/dependent/, or stdlib/epistemic/.