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 nWave-ai/nWave --skill nw-formal-verification-tlaplusgit clone --depth 1 https://github.com/nWave-ai/nWaveWrote 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/nwave-ai/nwave/nw-formal-verification-tlaplus)<a href="https://agentmods.dev/skills/nwave-ai/nwave/nw-formal-verification-tlaplus"><img src="https://agentmods.dev/badge/skills/nwave-ai/nwave/nw-formal-verification-tlaplus/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/nwave-ai/nwave/nw-formal-verification-tlaplus"><img src="https://agentmods.dev/badge/skills/nwave-ai/nwave/nw-formal-verification-tlaplus.svg" alt="Reviewed on agentmods" width="80" height="20"></a>- NVIDIA SkillSpector pass
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.00043 | $0.02176 |
| Opus 5 | $0.00022 | $0.01088 |
| Sonnet 5 | $0.00009 | $0.00435 |
| Haiku 4.5 | $0.00004 | $0.00218 |
Grade A, and why
nw-formal-verification-tlaplus 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 7d 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 — 211 lines — stays where its author put it; the contents beside it link to each section on GitHub.
Formal Verification with TLA+
When to Recommend Formal Verification
Decision Tree
Is the system distributed or concurrent?
|
+-- No --> Complex state machine with high failure cost?
| +-- No --> NOT cost-effective. Use property-based testing.
| +-- Yes --> CONSIDER TLA+
|
+-- Yes --> Consensus, coordination, or distributed transactions?
| +-- Yes --> RECOMMEND TLA+
| +-- No --> Could concurrency bug cause data loss or safety issues?
| +-- Yes --> RECOMMEND TLA+
| +-- No --> OFFER as option
Strong Indicators (Recommend)
| Domain | Why TLA+ Adds Value | Evidence |
|---|---|---|
| Distributed consensus (Paxos, Raft) | Subtle interleaving bugs in leader election | Raft TLA+ spec ~400 lines, found implementation bugs |
| Financial distributed transactions | Atomicity violations cause monetary loss | AWS DynamoDB replication verified |
| Leader election, distributed locking | Split-brain, deadlock, stale-lock | AWS lock manager verified |
| Eventual consistency / CRDTs | Convergence proofs required | TLA+ CRDT framework verifies SEC |
| Safety-critical state machines | Regulatory requirements | DO-178C, CENELEC recognize formal methods |
| Multi-party coordination (sagas, 2PC) | Compensation ordering, partial failure | 2PC is canonical TLA+ example |
| Data replication protocols | Ordering, consistency under failure | Elasticsearch, MongoDB, Cosmos DB verified |
When NOT to Use
- Simple CRUD (bugs are in implementation, not design)
- Single-process without complex state machines
- Prototypes/MVPs (design will change before verification completes)
- Performance optimization (TLA+ models correctness, not performance)
Cost-Benefit Reference
- Learning curve: 2-3 weeks to useful results (AWS engineers, all levels)
- Typical spec effort: 2-4 weeks part-time for a distributed protocol
- ROI highest when: bug cost is high, system is long-lived, protocol is novel, concurrency testing is impractical
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.
- 7d ago First seen · 211 lines · 43 tokens per session scan A 25471c340494
nw-formal-verification-tlaplus is a skill published in the GitHub repository nWave-ai/nWave (610 stars, last pushed 5d ago), licensed MIT. It adds 43 tokens to every session and 2,176 once invoked, about $0.0002 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-09-03.
Other skills, from other repositories
behavior-contract
Bug condition/postcondition formalization as testable Behavior Contracts. Defines invariants that must be preserved across fixes.
debugging
A structured method for finding and fixing software bugs. It starts by writing a test that reproduces the failure, then investigates its underlying cause before making a small fix.
hk-rca
Interactive Root Cause Analysis enforcer. Guides you through the 7-step RCA protocol: Reproduce, Locate, Hypothesis, Failing Test, Fix, Verify Live, Document. Use when debugging a bug, investigating a failure, or when something unexpected happened. This skill gates each step — it won't let you skip to a fix without…
debug-flow
Systematic debugging workflow. Reproduce the issue, isolate root cause, write a failing test, fix, verify. Use when diagnosing bugs or unexpected behavior.
test-driven-bug-fix
Defines reproduce-red-green-refactor bug fixes. Load when correcting a defect with a regression test.
team-fix
Runs the compressed bug-fix pipeline. Trigger on "run the bug-fix pipeline", "team-fix this bug", or "/team-fix" only; never infer pipeline intent from a plain bug-fix request.