Build and verify
Build a scoped change
Follow an example request through investigation, bug fixing, feature work, or a safe pause.
The z-mode router picks the matching playbook. Each one needs a different starting point.
| Work | Needs | Playbook |
|---|---|---|
| Bug | A repro and root cause | bug-fix |
| Feature | Observable acceptance | feature |
| Refactor | A held behavior contract | refactoring |
| Performance | A repeatable baseline | perf-issue |
/z-mode fix duplicate output; reproduce first; keep changes local$z-mode fix duplicate output; reproduce first; keep changes localKeep it clean
| Skill | Use it to |
|---|---|
| tdd | Add cheap, meaningful regressions. |
| no-comments | Run a reporting-only comment reviewer; the parent applies only authorized accepted edits. |
| unslop | Keep the explanation readable. |
| technical-writing | Apply the layered writing standard to docs, RFCs, PRs, and commit messages. |
Verify before publication
Use the project's existing harness first.
- create-verification-skill generates native project instructions from real launch, doctor, drive, evidence, and cleanup behavior, then executes one mapped path.
- maintain-verification-skill stays within that skill directory and reports product regressions.
- create-formal-verification-skill creates reusable checks for a stated invariant, with explicit bounds, code correspondence, and isolated broken variants that demonstrate detection. Invoke it explicitly for properties that user-path tests do not adequately cover; it is separate from the feature-map maintenance loop.
For example, check that two workers cannot both hold the same queue job's lease:
/create-formal-verification-skill check that at most one worker holds a job's lease; start with two workers and one job, and record the code correspondence and excluded behavior$create-formal-verification-skill check that at most one worker holds a job's lease; start with two workers and one job, and record the code correspondence and excluded behaviorA passing bounded model establishes the property within its modeled states and assumptions; it does not guarantee the implementation satisfies it. Review the code correspondence and retain those limits beside the result.
For event-order questions, the generator defaults to TLA+ regardless of implementation language, while retaining suitable existing project tooling. If no verifier supports the implementation language, it discloses the limitation and tests the real code with generated inputs instead of a handwritten function model. That fallback supplies reproducible test evidence, not formal proof.
Generated formal checks record covered files and functions and a last verified commit per check. After merges or refactors that skipped verification, explicitly invoke maintain-formal-verification-skill to review correspondence, update and rerun checks, and separate stale verification from real bugs. Blocked checks keep their previous checkpoint; dirty source gets separate snapshot evidence rather than a false HEAD checkpoint. Mutations stay in disposable copies, and product findings do not authorize product fixes.
Use explicitly invoked statechart to check a TLA+ model with TLC and explain it as readable states and the shortest path to each broken rule. A view module supplies the reader's labels, phases, and colors. It retains Mermaid source, a report, and TLC evidence, with optional browser-free Pele SVG rendering. It needs Node 22.18–22.x or 23.6+, Bun 1.1.5+, or Deno 2+, plus Java 11+ and TLA2TOOLS; without TLA2TOOLS it installs pinned TLC and Java through mise. Reproduce model findings against real code before calling them software bugs, and distinguish a model-level fix from a tested implementation fix.
Generated runtime verification skills already require a Helpers section with portable commands and an end-to-end run that confirms evidence survives cleanup. Check both when reviewing the generated skill.
Ask for proof you can inspect: real command output, a screenshot of the changed flow, a trace, or a readback of stored state. Match it to the acceptance check. A passing build alone does not prove changed behavior.
If the project already has a verify-<app> skill, name its real installed skill in the request. For example, with verify-export installed:
/z-mode reproduce the missing export row on the current main baseline with /verify-export; if it reproduces, fix it locally and show before/after row counts$z-mode reproduce the missing export row on the current main baseline with $verify-export; if it reproduces, fix it locally and show before/after row countsUse an isolated baseline checkout to preserve existing work. If the bug no longer reproduces, report that result. A generated verification skill needs an end-to-end proof before use; rerun maintenance when its map or harness drifts. Choose a maintenance cadence only when requested.
Vet a measured number
benchmark-checklist checks the limiter, production tuning, physical limits, correctness, alternating repeated runs, end-to-end relevance, and whether the timed work actually ran. It returns faster, slower, no measurable difference, or inconclusive, with the run count, range, and limiter; an inconclusive verdict names the evidence gap.
/benchmark-checklist vet this export speedup before it goes in the PR description$benchmark-checklist vet this export speedup before it goes in the PR descriptionThe Perf issue and Hillclimb playbooks already use the checklist. Invoke it directly for measurements made outside those workflows or for someone else's claim.
Publish on request
Each publication step needs its own request
Local edits, commit, push, PR, merge, and deployment are separate requested actions.
| Playbook | Runs when |
|---|---|
| Opening a PR | Publication is part of the request. |
| Babysit | You ask about status; status questions stay read-only. |
| Shipping | You grant explicit landing authority; it needs current-head evidence. |