By llm4rocq
Unified Rocq plugin (draft, formalize, autoformalize, prove, autoprove, checkpoint, review, refactor, golf, learn, doctor) — MCP-first, scripts fallback
npx claudepluginhub llm4rocq/rocq-skills --plugin rocqAutonomous end-to-end formalization from informal sources
Autonomous multi-cycle theorem proving with hard stop rules
Save progress with a safe commit checkpoint
Diagnostics, cleanup, and migration help
Draft Rocq declaration skeletons from informal claims
Interactive formalization — drafting plus guided proving
Improve Rocq proofs for directness, clarity, performance, and brevity
Interactive teaching and library exploration
Guided cycle-by-cycle theorem proving with explicit checkpoints
Leverage stdlib/MathComp, extract helpers, simplify proof strategies
Read-only code review of Rocq proofs
Strategic resolution of stubborn Admitted; may refactor across files within the header fence. Use when fast pass fails or for complex proofs.
Remove non-standard axioms by refactoring proofs. Use after checking axiom hygiene to systematically eliminate custom axioms.
Golf Rocq proofs after they compile; improve proofs for directness, clarity, performance, and brevity without changing semantics. Use after successful compilation to achieve 30-40% size reduction.
Compiler-guided iterative proof repair with two-stage repair escalation (fast → strong). Use for error-driven proof fixing with small sampling budgets (K=1).
Rocq (formerly Coq) workflow pack for AI coding agents. Gives your agent a structured prove/review/golf loop, library search, axiom checking, and safety guardrails. The workflows are host-agnostic — Claude Code, Codex, Gemini CLI, Cursor, and others all use the same core skill; only the invocation surface differs.
| Workflow | Description |
|---|---|
| draft | Draft Rocq declaration skeletons from informal claims |
| formalize | Interactive formalization — drafting plus guided proving |
| autoformalize | Autonomous end-to-end formalization from informal sources |
| prove | Guided cycle-by-cycle theorem proving |
| autoprove | Autonomous multi-cycle proving with stop rules |
| checkpoint | Save point (per-file + project build, axiom check, commit) |
| review | Read-only quality review |
| refactor | Leverage stdlib/MathComp, extract helpers, simplify proof strategies |
| golf | Improve proofs for directness, clarity, performance, and brevity |
| learn | Interactive teaching and library exploration |
| doctor | Diagnostics and migration help |
Claude Code: invoke as /rocq:<name>. Other hosts: follow the corresponding workflow in SKILL.md.
Typical session: draft (or formalize / autoformalize) → prove (or autoprove) → review → refactor → golf → checkpoint → git push.
draft — Skeleton-only drafting from informal claims. Use when you want Rocq declarations without a full prove run.formalize — Interactive synthesis. Drafts a skeleton, then runs guided prove cycles with user interaction.autoformalize — Autonomous synthesis. Extracts claims from a source, drafts skeletons, and proves them unattended.prove — Guided proof engine for existing declarations. Asks preferences at startup, prompts before each commit, pauses between cycles.autoprove — Autonomous proof engine for existing declarations. Auto-commits, loops until a stop condition fires (max cycles, max time, or stuck).Admitted gets a library search, tactic attempts, and validation. --commit controls per-fill commit behavior. When stuck, both force a review + replan.formalize and autoformalize wrap drafting around that same engine. Statement and header changes belong there — prove and autoprove keep declaration headers immutable..v files without a command activates the skill for one bounded pass — fix the immediate issue, then suggest the right next command: draft / formalize for statement work, prove / autoprove for proof work.See plugin README for the full command guide.
# TODO: Update once published to marketplace
/plugin install rocq
The skill works standalone with coqc, but is dramatically better with rocq-mcp — interactive proof sessions, parallel tactic testing, and sub-second feedback instead of full recompilation cycles.
What you get:
rocq_start — open interactive proof sessionrocq_check — execute tactics, see goalsrocq_step_multi — test multiple tactics in parallelrocq_compile — full file compilationrocq_query — Search, Check, Print, Aboutrocq_toc — file structure outlinerocq_notations — notation disambiguationrocq_verify — sandboxed proof verificationClaude Code (run from your Rocq project root):
# User-scoped — available in all your projects
claude mcp add --transport stdio --scope user rocq-mcp -- uvx rocq-mcp
# Or project-scoped — shared via .mcp.json
claude mcp add --transport stdio --scope project rocq-mcp -- uvx rocq-mcp
| Host | Status | Workflow |
|---|---|---|
| Claude Code | Full native | SKILL.md + scripts + /rocq:* commands, hooks, guardrails, subagents |
| Codex / Gemini / OpenCode | Documented* | SKILL.md + scripts |
| Cursor / Windsurf | Documented* | Project rules → SKILL.md + scripts |
*Documented setup patterns, not CI-verified.
MIT licensed. See LICENSE for more information.
Comprehensive UI/UX design plugin for mobile (iOS, Android, React Native) and web applications with design systems, accessibility, and modern patterns
Executes bash commands
Hook triggers when Bash tool is used
Uses power tools
Uses Bash, Write, or Edit tools
Ultra-compressed communication mode. Cuts ~75% of tokens while keeping full technical accuracy by speaking like a caveman.
Intelligent prompt optimization using skill-based architecture. Enriches vague prompts with research-based clarifying questions before Claude Code executes them
Persistent memory system for Claude Code - seamlessly preserve context across sessions
Standalone image generation plugin using Nano Banana MCP server. Generates and edits images, icons, diagrams, patterns, and visual assets via Gemini image models. No Gemini CLI dependency required.