Claude Code Skills for Software Correctness
Formal verification, model checking, security auditing, proof repair, and benchmarking — as slash commands.
Contents
Quick Start
Install every plugin in one command:
npx skills add workersio/spec
Individual plugins can be selected during installation. Once installed, invoke any skill by name inside Claude Code:
/fuzzer Coverage-guided fuzzing with audit-driven harness design
/kage Local pentest sandbox — recon, exploit, verify, judge, report
/kani-proof Write bounded model checker proofs for Rust and Solana
/solana-audit Run a structured smart contract security audit
/axiom Verify and repair Lean 4 proofs
/skill-benchmark Benchmark a skill with controlled eval sessions
/workers-app-tester Pentest an Android app on a rooted device
/save Save the current session as a reusable agent
Plugins
fuzzer
Coverage-guided fuzzing workflow for C/C++, Rust, and Go targets. Runs a deep audit-context-building pass first to locate suspicious code, then writes a targeted harness, builds with sanitizers, runs the fuzzer, and reports crashes with reproducers.
Use case — Find memory safety bugs, integer overflows, and logic faults in native code through coverage-guided fuzzing driven by prior code understanding.
/fuzzer
What's included
fuzzer skill — end-to-end harness authoring, build, run, and triage workflowaudit-context-building skill — line-by-line analysis using First Principles, 5 Whys, and 5 Hows to locate fuzz targets- Function-analyzer agent and reference docs for completeness, output requirements, and worked micro-analysis examples
kage
Local pentest sandbox that runs a full black-box engagement end-to-end. Every tool runs inside a per-engagement Kali Docker container, so each working directory gets its own isolated sandbox with no cross-contamination. Recon, deep testing, exploit verification, chain-building, judging, and report writing all happen through sub-agents coordinated from a single skill.
Use case — Run a complete black-box, greybox, or white-box security audit on a target domain or source path and get a deduplicated, verified findings report at ./results/<target>/audit-report.md.
/kage
What's included
- Per-engagement Kali container with a
k shim for concurrent, isolated runs
- Parallel tester sub-agents (auth, IDOR, access control, SSRF, injection, client-side, API, logic, content discovery, headers, JS secrets, port scanner, vuln scanner)
- Verifier, chain-builder, judge, and report-writer agents for reproducible PoCs and a filtered, scored final report
- Reference docs for methodology, 4-gate judging, 7 escalation-chain patterns, platform report formatting, and the bundled audit-context-building greybox workflow
- Dockerfile, compose file, dork list, credentials template, and wordlist strategy
kani-proof
Writes Kani bounded model checker proofs for Rust and Solana programs. Generates proof harnesses, loop invariants, and property checks. Includes reference docs for proof patterns, invariant design, coverage workflows, Kani features, and Anchor program verification.
Use case — Prove absence of panics, arithmetic overflows, and unsafe memory access in Rust code. Verify Solana program logic with bounded inputs.
/kani-proof
What's included
- Proof pattern references for common Rust constructs
- Invariant design guides for loops and recursion
- Coverage workflow for measuring proof completeness
- Anchor-specific verification patterns for Solana programs
- Kani feature reference (stubs, contracts, harness configuration)
solana-audit
