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.
Install with Tessl CLI
npx tessl i github:ArabelaTso/Skills-4-SE --skill formal-spec-generator80
Does it follow best practices?
If you maintain this skill, you can automatically optimize it using the tessl CLI to improve its score:
npx tessl skill review --optimize ./path/to/skillValidation for skill structure
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 follows best practices. It provides comprehensive coverage of capabilities with specific actions, includes explicit 'Use when' guidance with multiple trigger scenarios, uses appropriate third-person voice throughout, and targets a clear niche (formal verification with Isabelle/HOL and Coq) that distinguishes it from other skills.
| 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 various inputs) AND when with explicit 'Use when users need to:' clause followed by six specific trigger scenarios. The structure is exemplary for completeness. | 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', 'mathematical concepts'. These cover the domain well and match how users in this field would phrase requests. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive with clear niche in formal verification using Isabelle/HOL and Coq. The specific mention of these proof assistants and formal methods terminology (predicates, invariants, pre/post-conditions) makes it 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 suffers from being somewhat verbose and lacking concrete inline examples. The workflow is clear but missing validation steps for ensuring generated specifications are syntactically correct. The progressive disclosure structure is well-executed with appropriate references to detailed pattern files.
Suggestions
Add at least one complete, concrete inline example showing the transformation from informal requirement to formal specification (e.g., the max element example should show the actual Isabelle/Coq code, not just describe what it should contain)
Add explicit validation steps in the workflow, such as 'Verify syntax by checking that all parentheses/brackets match and all required imports are included'
Remove explanatory content Claude already knows (e.g., definitions of informal requirements, source code, pseudocode) and condense the Key Principles section which largely restates general good coding practices
| 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 about writing clear, correct code. | 2 / 3 |
Actionability | Provides structural templates for Isabelle and Coq output, but lacks concrete executable examples inline. The actual worked examples are deferred to a reference file, and the inline code blocks are templates with placeholders rather than copy-paste ready specifications. | 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 'Test syntax' being mentioned only as a tip at the end. | 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. The main file provides enough context while appropriately deferring detailed patterns and examples to reference files. | 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.
- 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.