proof-refactoring-assistant
Restructure and improve Isabelle or Coq proofs to enhance readability, modularity, and maintainability without changing semantics. Use when proofs are long and monolithic, have repeated patterns, use unclear naming, lack documentation, or when the user asks to refactor, clean up, improve, or reorganize their formal proofs.
91
86%
Does it follow best practices?
Impact
100%
1.00xAverage score across 3 eval scenarios
Passed
No known issues
Quality
Discovery
100%Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.
This is an excellent skill description that clearly defines its scope (Isabelle/Coq proof refactoring), lists concrete improvement goals, and provides comprehensive trigger conditions. The explicit 'Use when...' clause covers both problem states and user intent phrases, making it highly actionable for skill selection.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'Restructure', 'improve', 'enhance readability, modularity, and maintainability'. Also specifies the domain clearly as 'Isabelle or Coq proofs'. | 3 / 3 |
Completeness | Clearly answers both what (restructure/improve proofs for readability, modularity, maintainability) AND when (explicit 'Use when...' clause with multiple trigger scenarios including user intent phrases). | 3 / 3 |
Trigger Term Quality | Excellent coverage of natural terms users would say: 'refactor', 'clean up', 'improve', 'reorganize', 'formal proofs', plus problem descriptions like 'long and monolithic', 'repeated patterns', 'unclear naming'. | 3 / 3 |
Distinctiveness Conflict Risk | Very clear niche targeting specifically 'Isabelle or Coq proofs' - formal theorem proving languages. Unlikely to conflict with general code refactoring skills due to the specific domain terminology. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
72%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This is a well-structured skill with excellent actionability through concrete before/after code examples in both Coq and Isabelle. The progressive disclosure is good with appropriate external references. However, the content is somewhat verbose with explanatory text that Claude doesn't need, and the workflow could benefit from more explicit validation commands and feedback loops for the refactoring process.
Suggestions
Trim explanatory prose in the workflow steps - Claude understands concepts like 'preserve semantics' and 'incremental changes' without elaboration
Add explicit validation commands in Step 3, such as specific compilation commands for Isabelle (isabelle build) and Coq (coqc) with expected success indicators
Condense the 'Refactoring Guidelines' and 'Best Practices' sections which overlap significantly and contain guidance Claude would naturally follow
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The skill is moderately efficient but includes some unnecessary verbosity. The workflow steps and guidelines sections contain explanatory text that Claude would already understand (e.g., explaining what 'preserve semantics' means). The content could be tightened significantly while retaining all actionable guidance. | 2 / 3 |
Actionability | The skill provides excellent concrete, executable examples with before/after code in both Coq and Isabelle. Each refactoring pattern is illustrated with copy-paste ready code showing the transformation, making it immediately actionable. | 3 / 3 |
Workflow Clarity | The 4-step workflow is clearly sequenced, but validation checkpoints are implicit rather than explicit. Step 3 mentions 'Test continuously' and 'Recompile after each change' but doesn't provide specific commands or explicit feedback loops for error recovery in the refactoring process. | 2 / 3 |
Progressive Disclosure | The skill has good structure with a clear overview, quick reference table, detailed examples, and appropriate references to external files (refactoring_patterns.md). Navigation is clear with one-level-deep references and well-organized sections. | 3 / 3 |
Total | 10 / 12 Passed |
Validation
100%Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.
Validation — 11 / 11 Passed
Validation for skill structure
No warnings or errors.
- Repository
- ArabelaTso/Skills-4-SE
- Commit
0f00a4f
- Reviewed
Table of Contents
Is this your skill?
If you maintain this skill, you can claim it as your own. Once claimed, you can manage eval scenarios, bundle related skills, attach documentation or rules, and ensure cross-agent compatibility.