Claude Code Skills for Software Correctness
Formal verification, model checking, security auditing, proof repair, and benchmarking — as slash commands.
- Quick Start
- Plugins
- kani-proof — Model checking for Rust and Solana
- solana-audit — Smart contract security audits
- axiom — Lean 4 proof verification and repair
- skill-benchmark — Measure whether a skill actually helps
- workers-app-tester — Mobile application security testing
- save — Convert sessions into reusable agents
- Repository Structure
- Contributing
- License
Install every plugin in one command:
npx skills add workersio/specIndividual plugins can be selected during installation. Once installed, invoke any skill by name inside Claude Code:
/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
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)
Structured security audits for Solana smart contracts covering 25 vulnerability types. Walks through each attack vector systematically — from missing signer checks and PDA validation to re-initialization attacks and arithmetic overflows.
Use case — Audit Solana programs before deployment. Identify vulnerabilities across the full attack surface for on-chain programs.
/solana-audit
What's included
- Per-vulnerability reference docs for all 25 audit categories
- Audit checklist for systematic coverage
- Cheatsheet for quick reference during review
- Exploit case studies from real-world incidents
Verify, check, transform, and repair Lean 4 proofs using the Axiom (Axle) API and CLI. Submits proof terms to the Axiom kernel for type-checking and returns structured verification results.
Use case — Machine-check mathematical proofs and formal specifications. Validate and repair proof steps during interactive theorem proving.
/axiom
Benchmark any agent skill to measure whether it actually improves performance. Runs isolated eval sessions with and without the target skill, grades outputs via layered grading (deterministic checks + LLM-as-judge), analyzes behavioral signals, and generates a comparison report with a USE / DON'T USE verdict.
Use case — Objectively measure whether a skill helps or hurts on a specific class of tasks before committing to it.
/skill-benchmark
What's included
- Runner agent for executing controlled eval sessions
- Grader agent with layered grading (deterministic + LLM-as-judge)
- Reporter agent for generating comparison reports
- Scripts for stream parsing, transcript analysis, and check execution
- Configuration reference and directory structure docs
Penetration test Android applications on a rooted device. Drives the UI over ADB, intercepts HTTPS traffic through mitmproxy, bypasses SSL pinning with Frida, decompiles APKs for static analysis, and runs security checks for IDORs, auth issues, data exposure, and hardcoded secrets.
Use case — Security test mobile applications for common vulnerabilities before release.
/workers-app-tester
What's included
- UI parsing and automation scripts for ADB
- Traffic capture and analysis tooling via mitmproxy
- Universal SSL pinning bypass with Frida
- Static analysis through APK decompilation
Converts Claude Code conversations into reusable agents. Analyzes the current session — the original task, every correction, tool calls, and final output — and distills it into an agent file saved to .claude/agents/. Agents are invocable with @agent-name in future sessions and shared through version control. No server, no API, no accounts.
Use case — Capture a working workflow once, replay it forever.
/save
.claude-plugin/marketplace.json Root marketplace catalog
plugins/
kani-proof/ Bounded model checking for Rust
.claude-plugin/plugin.json
skills/kani-proof/SKILL.md
skills/kani-proof/references/
solana-audit/ Solana smart contract audits
.claude-plugin/plugin.json
skills/solana-audit/SKILL.md
skills/solana-audit/references/
axiom/ Lean 4 proof verification
.claude-plugin/plugin.json
skills/axiom/SKILL.md
skill-benchmark/ Benchmark agent skills
.claude-plugin/plugin.json
skills/skill-benchmark/SKILL.md
skills/skill-benchmark/scripts/
skills/skill-benchmark/agents/
skills/skill-benchmark/references/
workers-app-tester/ Mobile app security testing
.claude-plugin/plugin.json
skills/workers-app-tester/SKILL.md
skills/workers-app-tester/scripts/
skills/workers-app-tester/references/
save/ Session-to-agent converter
.claude-plugin/plugin.json
skills/save/SKILL.md
Each plugin is self-contained under plugins/ with its own manifest and skill definitions. The root marketplace.json registers all plugins for discovery via npx skills.
Contributions welcome. To add a new plugin:
- Create a directory under
plugins/ - Add a
.claude-plugin/plugin.jsonmanifest - Define skills under
skills/<skill-name>/SKILL.md - Register the plugin in
.claude-plugin/marketplace.json
See any existing plugin for the expected structure.