program-to-model-extractor
Extract abstract mathematical models from functional code (Haskell, OCaml, F#) for formal reasoning in Isabelle/HOL. Use when users need to: (1) Convert functional programs to Isabelle definitions, (2) Extract high-level algorithm essence from implementation code, (3) Generate formal specifications and properties from code, (4) Create verification-ready models that capture mathematical properties while abstracting away implementation details. Focuses on structural recursion, algebraic data types, higher-order functions, and invariant extraction.
Install with Tessl CLI
npx tessl i github:ArabelaTso/Skills-4-SE --skill program-to-model-extractor89
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 clearly defines a specialized niche at the intersection of functional programming and formal verification. It provides comprehensive coverage of capabilities, explicit trigger conditions with numbered use cases, and domain-specific terminology that users in this field would naturally use. The description is well-structured, uses proper third-person voice, and would be easily distinguishable from other skills.
| Dimension | Reasoning | Score |
|---|---|---|
Specificity | Lists multiple specific concrete actions: 'Convert functional programs to Isabelle definitions', 'Extract high-level algorithm essence', 'Generate formal specifications and properties', 'Create verification-ready models'. Also specifies focus areas: structural recursion, algebraic data types, higher-order functions, invariant extraction. | 3 / 3 |
Completeness | Clearly answers both what ('Extract abstract mathematical models from functional code for formal reasoning') AND when with explicit 'Use when users need to:' clause followed by four numbered trigger scenarios. The structure explicitly addresses both questions. | 3 / 3 |
Trigger Term Quality | Includes natural keywords users would say: 'Haskell', 'OCaml', 'F#', 'Isabelle/HOL', 'formal reasoning', 'verification', 'algebraic data types', 'higher-order functions'. Covers both language names and domain-specific terms a user working in this space would naturally use. | 3 / 3 |
Distinctiveness Conflict Risk | Highly distinctive niche combining functional programming languages (Haskell, OCaml, F#) with formal verification (Isabelle/HOL). Very unlikely to conflict with other skills due to the specialized domain of formal methods and theorem proving. | 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 strong actionability through concrete Isabelle code examples and good progressive disclosure via external references. The main weaknesses are some verbosity in explanatory sections and missing validation steps in the extraction workflow—users should know how to verify their extracted models compile and type-check in Isabelle.
Suggestions
Add validation checkpoint after step 3 or 4: 'Load the theory file in Isabelle and verify all definitions are accepted before proceeding to properties'
Trim the Overview section—Claude understands what mathematical abstraction means; jump directly to the workflow
| Dimension | Reasoning | Score |
|---|---|---|
Conciseness | The content is mostly efficient but includes some unnecessary explanation in the Overview section that Claude would already understand. The 'Abstraction Guidelines' section with checkmarks is helpful but slightly verbose. | 2 / 3 |
Actionability | Provides fully executable Isabelle code examples throughout, with concrete syntax for datatypes, functions, and lemmas. The complete quicksort extraction example is copy-paste ready and demonstrates the full workflow. | 3 / 3 |
Workflow Clarity | The 5-step workflow is clearly sequenced, but lacks explicit validation checkpoints. There's no guidance on verifying that extracted models are correct or how to handle extraction errors—important for formal verification work. | 2 / 3 |
Progressive Disclosure | Excellent structure with a clear overview, inline examples for quick reference, and well-signaled one-level-deep references to extraction_patterns.md and isabelle_syntax.md for detailed patterns. | 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.
- 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.