formal-spec-generator
Generate formal specifications (definitions, predicates, invariants, pre/post-conditions) in Isabelle/HOL or Coq from informal requirements, source code, pseudocode, or mathematical descriptions. Use when users need to: (1) Formalize algorithms or data structures, (2) Create function specifications with contracts, (3) Generate predicates and properties for verification, (4) Translate informal requirements into formal logic, (5) Specify invariants for loops or data structures, or (6) Create formal definitions for mathematical concepts. Supports both Isabelle/HOL and Coq equally.
86
78%
Does it follow best practices?
Impact
99%
1.00xAverage score across 3 eval scenarios
Passed
No known issues
Optimize this skill with Tessl
npx tessl skill review --optimize ./skills/formal-spec-generator/SKILL.mdQuality
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 articulates specific capabilities in formal specification generation, provides comprehensive trigger scenarios with an explicit 'Use when' clause, and targets a distinctive technical niche. The description uses proper third-person voice throughout and covers both supported proof assistants equally.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'Generate formal specifications (definitions, predicates, invariants, pre/post-conditions)', 'Formalize algorithms or data structures', 'Create function specifications with contracts', 'Generate predicates and properties for verification', 'Translate informal requirements into formal logic', 'Specify invariants for loops or data structures'. | 3 / 3 |
Completeness | Clearly answers both what ('Generate formal specifications...from informal requirements, source code, pseudocode, or mathematical descriptions') and when with explicit 'Use when users need to:' clause followed by six specific trigger scenarios. | 3 / 3 |
Trigger Term Quality | Includes strong natural keywords users would say: 'Isabelle/HOL', 'Coq', 'formal specifications', 'predicates', 'invariants', 'pre/post-conditions', 'verification', 'formal logic', 'contracts'. These cover the domain well and match how users in formal methods would naturally describe their needs. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche targeting formal verification with specific proof assistants (Isabelle/HOL, Coq). The technical domain is narrow enough that it's unlikely to conflict with general coding or documentation skills. | 3 / 3 |
Total | 12 / 12 Passed |
Implementation
57%Reviews the quality of instructions and guidance provided to agents. Good implementation is clear, handles edge cases, and produces reliable results.
This skill provides a reasonable framework for generating formal specifications but relies too heavily on abstract descriptions rather than concrete, executable examples. The progressive disclosure is well-handled with clear references to supporting files, but the main content would benefit from inline worked examples and explicit validation steps to ensure generated specifications are syntactically correct.
Suggestions
Add at least one complete, executable inline example showing the full transformation from informal requirement to formal specification (rather than deferring all examples to references/examples.md)
Include explicit validation steps in the workflow, such as 'Verify the generated code parses correctly in the target system before presenting to user'
Remove explanatory content Claude already knows (e.g., definitions of informal requirements, source code, pseudocode) and condense the Key Principles section
Replace the abstract 'Common Patterns' descriptions with concrete before/after examples showing actual input and generated output
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The content is reasonably efficient but includes some unnecessary explanation (e.g., explaining what informal requirements, source code, and pseudocode are). The workflow steps could be more condensed, and some sections like 'Key Principles' contain guidance Claude already knows. | 2 / 3 |
Actionability | Provides structural templates for Isabelle and Coq output, but the code examples are incomplete templates rather than executable specifications. The 'Common Patterns' section describes what to do abstractly rather than showing concrete, copy-paste ready examples inline. | 2 / 3 |
Workflow Clarity | The 5-step workflow is clearly sequenced, but lacks validation checkpoints. There's no guidance on verifying that generated specifications are syntactically valid or semantically correct before presenting to users, despite the 'Test syntax' tip being mentioned only briefly. | 2 / 3 |
Progressive Disclosure | Excellent structure with clear overview and well-signaled one-level-deep references to isabelle_patterns.md, coq_patterns.md, and examples.md. Content is appropriately split between the main skill file and reference materials. | 3 / 3 |
Total | 9 / 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.