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.

1.00x

Quality

74%

Does it follow best practices?

Impact

99%

1.00x

Average score across 3 eval scenarios

Securityby

Passed

No findings from the security scan

Fix and improve this skill with Tessl

tessl review fix ./skills/formal-spec-generator/SKILL.md

Quality

Content

63%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.

Well-organized with excellent progressive disclosure to real bundled references, but the inline templates are placeholders rather than executable code and the workflow lacks validation checkpoints for generated formal code.

Suggestions

Replace the placeholder Isabelle/Coq templates with at least one complete executable example inline, or explicitly direct the model to copy a concrete pattern from the reference files before filling it in.

Add a validation checkpoint in the workflow (e.g., 'Type-check / load the theory in Isabelle or Coq; fix syntax errors before delivering') with a fix-and-retry loop, since generated specifications must be syntactically valid.

Trim 'Key Principles' and 'Tips' entries that restate common knowledge (use standard libraries, prefer simple definitions, start simple) to reduce token overhead.

Dimension	Reasoning	Score
Conciseness	Largely efficient with a well-structured workflow and minimal padding, though some sections like 'Key Principles' and 'Tips' restate generic guidance (use libraries, start simple) Claude already knows.	4 / 5
Actionability	Provides skeleton code templates for both systems, but they are placeholder pseudocode ('datatype ...', 'fun ... where ...') rather than executable copy-paste examples; the actual runnable examples live only in the bundled reference files.	3 / 5
Workflow Clarity	A clear five-step sequence is present, but there are no validation or verification checkpoints (e.g., type-checking or 'sorry'/'Admitted' confirmation) despite the skill generating code that must be syntactically valid, so the cap applies.	3 / 5
Progressive Disclosure	Clear overview in SKILL.md with well-signaled, one-level-deep links to real bundled files (isabelle_patterns.md, coq_patterns.md, examples.md), all of which exist, splitting detail appropriately.	5 / 5
	Total	15 / 20 Passed

Description

85%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.

A strong, third-person description that clearly states both capability and an explicit six-item 'Use when' trigger list. Minor gaps in action diversity and synonyms keep it just below perfect.

Dimension	Reasoning	Score
Specificity	Lists several concrete actions ('Generate formal specifications (definitions, predicates, invariants, pre/post-conditions)') but the actions are the same artifact type repeated, leaving minor coverage gaps rather than multiple distinct concrete actions.	4 / 5
Completeness	Explicitly answers both what ('Generate formal specifications... in Isabelle/HOL or Coq') and when ('Use when users need to: (1)...(6)') with concrete numbered trigger phrases.	5 / 5
Trigger Term Quality	Strong natural terms ('formal specifications', 'invariants', 'pre/post-conditions', 'Isabelle/HOL', 'Coq') with numbered user-facing triggers, though it lacks synonyms or file extensions common users might say.	4 / 5
Distinctiveness Conflict Risk	The formal-spec niche is fairly distinct and tied to named proof assistants, but the broad 'formalize algorithms/requirements' framing has minor overlap risk with general code-generation or verification skills.	4 / 5
	Total	17 / 20 Passed

Validation

100%

Warnings & errors only

Checks the skill against the spec for correct structure and formatting. All validation checks must pass before discovery and implementation can be scored.

Validation — 16 / 16 Passed

Validation for skill structure

No warnings or errors.

Repository: ArabelaTso/Skills-4-SE
Path: skills/formal-spec-generator/SKILL.md
Commit: 4f38503

Reviewed: 8 days ago

Table of Contents

Discovery Implementation Validation

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.