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.
git clone --depth 1 https://github.com/punt-labs/z-specWrote 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/commands/punt-labs/z-spec/refine-dev)<a href="https://agentmods.dev/commands/punt-labs/z-spec/refine-dev"><img src="https://agentmods.dev/badge/commands/punt-labs/z-spec/refine-dev/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/commands/punt-labs/z-spec/refine-dev"><img src="https://agentmods.dev/badge/commands/punt-labs/z-spec/refine-dev.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.00014 | $0.10618 |
| Opus 5.5 | $0.00006 | $0.04247 |
| Sonnet 5.5 | $0.00003 | $0.02124 |
| Haiku 4.5 | $0.00001 | $0.01062 |
Grade A, and why
refine-dev 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 — 1,533 lines — stays where its author put it; the contents beside it link to each section on GitHub.
/z-spec-dev:refine-dev - Data Refinement Verification
Verify that implementation code correctly refines a Z specification by defining an abstraction function and generating commutativity tests (and optionally Lean 4 proofs) for every operation.
The key correctness property for each operation:
abstract(concreteOp(concreteState)) = abstractOp(abstract(concreteState))
If this holds for every operation, the code is a provably correct refinement of the specification.
Input
Arguments: $ARGUMENTS
Parse arguments:
- First positional argument: Z specification file (default: search
docs/*.tex) - Second positional argument: target language (default: auto-detect)
--lean- also generate Lean 4 commutativity proofs inproofs/--generate-abstraction- auto-generate abstraction function scaffold (otherwise walk the user through defining it interactively)--impl <file>- path to implementation file (default: auto-detect from project)
Process
0. Prerequisites
Verify the specification has been type-checked:
which fuzz >/dev/null 2>&1 || echo "FUZZ_NOT_FOUND"
If fuzz is not found: Warn but do not block. The refinement
process can proceed without type-checking, but recommend running
/z-spec-dev:check-dev first.
If --lean is specified, verify Lean 4 and Lake are installed:
which lean >/dev/null 2>&1 || echo "LEAN_NOT_FOUND"
which lake >/dev/null 2>&1 || echo "LAKE_NOT_FOUND"
If lean or lake not found: Stop and tell the user:
Lean 4 is not installed. Run
/z-spec-dev:setup-dev leanto install the Lean 4 toolchain via elan. Or omit--leanto generate commutativity tests only.
The Z specification should already exist. Implementation code
should also exist (from /z-spec-dev:model2code-dev or hand-written).
1. Locate the Specification
If a file path is provided, use it directly.
If no file specified:
- Look in
docs/for.texfiles containing Z specifications - If multiple found, ask user to specify
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 · 1,533 lines · 14 tokens per session scan A 7b104c55efa2
refine-dev is a command published in the GitHub repository punt-labs/z-spec (5 stars, last pushed 4d ago), licensed MIT. It adds 14 tokens to every session and 10,618 once invoked, about $0.0001 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-31.
Other commands, from other repositories
feedback-to-us
Tell us how the prfaq plugin is working for you (anonymous 1-5 feedback).
badge
Generate a stage-colored badge and embed it in your README.
import
Import an existing document and launch the full /prfaq workflow with extracted content.
research
Research evidence for PR/FAQ claims and generate biblatex citations.
review
Peer review a PR/FAQ document for quality and decision readiness.
streamline
Tighten a PR/FAQ by removing redundancy, weasel words, and bloat.