CtrlK
BlogDocsLog inGet started
Tessl Logo

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.

81

1.00x
Quality

71%

Does it follow best practices?

Impact

100%

1.00x

Average score across 3 eval scenarios

SecuritybySnyk

Passed

No findings from the security scan

Fix and improve this skill with Tessl

tessl review fix ./skills/proof-refactoring-assistant/SKILL.md
SKILL.md
Quality
Evals
Security

Quality

Content

60%Weight 40%Scale 1-5

Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.

The content is well-structured and actionable, with solid before/after proof examples, a sequenced workflow, and checklists, all backed by a real one-level reference file. Its main weakness is conciseness: the patterns and guidance are repeated across multiple sections, making the body longer than it needs to be.

Suggestions

Collapse the redundancy between the Step 2 pattern criteria, the "Common Refactoring Patterns" pointer, and the Quick Reference table into a single consolidated pattern list so each pattern appears once.

Add the concrete verification command(s) — e.g. `isabelle build -D .` and `coqc foo.v` — to the "Test continuously" step so the workflow is fully executable and the feedback loop is explicit (compile fails → fix → recompile).

Move most of the six before/after examples and the guidelines/best-practices/anti-patterns material into references/refactoring_patterns.md, leaving SKILL.md a lean overview that points to the catalog.

DimensionReasoningScore

Conciseness

The ~340-line body is noticeably verbose: the Overview restates the description and the ten refactoring patterns are repeated across Step 2 bullet-criteria, the Quick Reference table, and the examples, creating several padded/redundant sections. It does not rise to a 3 because the repetition is substantial rather than a single tighten-up spot.

2 / 5

Actionability

Six concrete before/after Coq and Isabelle code examples with per-pattern application criteria give mostly executable guidance; the gap is that "Test continuously: Recompile after each change" never supplies the actual compile command (isabelle build / coqc), so it stops short of fully copy-paste ready.

4 / 5

Workflow Clarity

A clear four-step sequence (Analyze → Identify → Apply → Verify) with checklists (Before/During/After) and an explicit "verify after each change" checkpoint; the error-recovery feedback loop (fail → fix → re-validate) is only implied rather than spelled out, a minor validation gap.

4 / 5

Progressive Disclosure

Good structure with clearly signaled, one-level-deep references to the real references/refactoring_patterns.md and navigable section headers; the body still inlines substantial detail (six full code examples plus overlapping guideline/best-practice/anti-pattern sections) that keeps it from being a lean 5-overview.

4 / 5

Total

14

/

20

Passed

Description

82%Weight 40%Scale 1-5

Based on the skill's description, can an agent find and select it at the right time? Clear, specific descriptions lead to better discovery.

The description is strong: it clearly states what the skill does, gives explicit multi-trigger "Use when" guidance, and occupies a distinctive niche. Its only weakness is that the action verbs (restructure/improve) are somewhat abstract rather than enumerating concrete refactoring operations.

DimensionReasoningScore

Specificity

Names the domain ("Isabelle or Coq proofs") and a couple of actions ("Restructure and improve"), but the verbs are abstract rather than concrete like "extract"/"fill"/"merge", so it is not comprehensive enough for a 4.

3 / 5

Completeness

Explicitly answers what ("Restructure and improve Isabelle or Coq proofs…without changing semantics") and when ("Use when proofs are long and monolithic, have repeated patterns, use unclear naming, lack documentation, or when the user asks to refactor…") with concrete trigger phrases.

5 / 5

Trigger Term Quality

Strong natural trigger coverage with synonyms ("refactor, clean up, improve, or reorganize their formal proofs") plus descriptive smell-triggers, but no file extensions (.thy/.v) or terms like "tidy up", so it falls just short of comprehensive.

4 / 5

Distinctiveness Conflict Risk

Targets a narrow, well-defined niche (formal-proof refactoring in Isabelle/Coq) with triggers unlikely to fire for unrelated skills, giving minimal conflict risk.

5 / 5

Total

17

/

20

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.

Validation16 / 16 Passed

Validation for skill structure

No warnings or errors.

Repository
ArabelaTso/Skills-4-SE
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.