benbrastmckie/nvim/skill-cslib-research
Claude Code and agent skill by benbrastmckie/nvim
- community
Checking that the SKILL.md file is still in the repository.
Research CSLib formalization patterns and Mathlib API for CSLib contributions. Invoke for cslib research tasks.
Install
npx vskill@latest install benbrastmckie/nvim/skill-cslib-researchSKILL.md
CSLib Research Skill
Thin wrapper that delegates CSLib research to cslib-research-agent subagent.
Trigger Conditions
This skill activates when:
- Task type is "cslib"
- Research is needed for CSLib formalization, Lean 4 proof patterns, or Mathlib API
- CSLib contribution standards or module patterns need to be gathered
Execution Flow
Stage 1: Input Validation
Validate task_number exists and task_type is "cslib".
Stage 2: Preflight Status Update
Update status to "researching" BEFORE invoking subagent.
Stage 3: Prepare Delegation Context
Domain-specific context for the cslib-research-agent:
- lean-lsp MCP tools for Mathlib search (lean_leansearch, lean_loogle, lean_local_search)
- CSLib context files from
.claude/extensions/cslib/context/ - Local CSLib Lean files for pattern analysis
Stage 4a: Memory and Literature Retrieval (Auto)
Retrieve relevant memories and literature briefing to inject into the delegation context.
Skip memory if: clean_flag is true (from --clean command flag).
Note: lit_flag is independent of clean_flag. Using --clean --lit suppresses memory retrieval but still injects literature briefing. Literature briefing is gated solely on lit_flag == "true".
Stage 4: Invoke Subagent
Use Agent tool with subagent_type: "cslib-research-agent".
Include memory_context and lit_context in the prompt if non-empty:
- If
memory_contextis non-empty, include it as a<memory-context>block after the delegation context. - If
lit_contextis non-empty, include it as a<literature-briefing>block after the memory context.
Stage 4b: Self-Execution Fallback
CRITICAL: If you performed the work above WITHOUT using the Agent tool (i.e., you read files, wrote artifacts, or updated metadata directly instead of spawning a subagent), you MUST write a .return-meta.json file now before proceeding to postflight. Use the schema from return-metadata-file.md with the appropriate status value for this operation.
If you DID use the Agent tool, skip this stage -- the subagent already wrote the metadata.
Postflight (ALWAYS EXECUTE)
The following stages MUST execute after work is complete, whether the work was done by a subagent or inline (Stage 4b). Do NOT skip these stages for any reason.
Stage 5: Parse Subagent Return
Read the metadata file from specs/{N}_{SLUG}/.return-meta.json.
Expected `status` vocabulary: researched on success; otherwise partial, failed, or blocked. This is a closed set (@.claude/context/formats/return-metadata-file.md is normative) and near-synonyms are not accepted — see the status note in cslib-research-agent.md's Stage 7 for the three consumers a variant breaks and the stranded-task failure mode it produces. If the value read here is outside the set, do NOT proceed to Stage 6 as if it were a success: report it and stop, so the task is not promoted on an unrecognized outcome.
No `.orchestrator-handoff.json`: research agents never write one, in any mode, including under orchestrator_mode: true (cslib-research-agent.md Stage 7 states this as a prohibition). A dispatching orchestrator MUST NOT instruct this skill's subagent to write one either — .return-meta.json is the sole status channel for research, and skill-orchestrate's Stage 5 already treats an absent handoff from a research dispatch as the expected outcome and recovers through scripts/orchestrate-recover-outcome.sh.
Defensive case, if this prohibition is ever reversed: should a future variant of this skill's subagent write .orchestrator-handoff.json, it MUST echo dispatch_seq unchanged from its own delegation context — copy the value verbatim (never invent, increment, or recompute one), or omit it when the delegation context omits it. See context/patterns/dispatch-report-not-termination.md.
Stage 6: Update Task Status (Postflight)
Update state.json and TODO.md based on result.
Stage 7: Link Artifacts
Add research artifact to state.json. Update TODO.md per @.claude/context/patterns/artifact-linking-todo.md with field_name=**Research**, next_field=**Plan**.
Stage 8: Git Commit
Commit changes with session ID.
Stage 9: Return Brief Summary
Return Format
Brief text summary (NOT JSON).
Security
- Security scanPassed, 100 of 100Pattern checks on the skill's files.
- Model reviewNot runA model review is scheduled for the next rescan.
Quality evaluation
- Task evaluationNot runNo evaluation yet. Run one in Skill Studio.
Source
- SKILL.md in the repositoryCheckingagent-system/extensions/cslib/skills/skill-cslib-research/SKILL.md
Popularity
- Repository stars
- 444
- Repository forks
- 464
- 7-day trend score
- 30
Stars and forks are for the whole GitHub repository, not this skill alone. Not refreshed yet.
Works with
Any agent vskill installs to: 56 targets in all. These 39 have a page on this site.
- Claude Code
- Cursor
- GitHub Copilot
- Windsurf
- Codex
- Gemini CLI
- Cline
- Amp
- Roo Code
- Goose
- Continue
- Kilo Code
- Junie
- Trae
- OpenHands
- Qwen Code
- AI Agent
- Tabnine Chat
- Sourcegraph Cody
- Amazon Q
- Firebase Genkit
- Sweep
- Devin
- Phind
- Mentat
- Claude Desktop
- Aider
- GPT Pilot
- Plandex
- bolt.new
- v0
- Replit Agent
- Anse
- TypingMind
- BetterChatGPT
- LibreChat
- Warp AI
- Pieces
- Fig AI
Embed badge
[](https://verified-skill.com/skills/benbrastmckie/nvim/skill-cslib-research)