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

78%

Does it follow best practices?

Impact

99%

1.00x

Average score across 3 eval scenarios

Securityby

Passed

No known issues

Optimize this skill with Tessl

npx tessl skill review --optimize ./skills/formal-spec-generator/SKILL.md

Evaluation results

100%

Formalizing a Queue Data Structure

Source code formalization workflow

Criteria

Without context

With context

Isabelle file produced

100%

Coq file produced

100%

Isabelle theory structure

100%

Coq imports structure

100%

Queue data type defined

100%

Operation functions defined

100%

Preconditions specified

100%

Postconditions specified

100%

Isabelle sorry for theorems

100%

Coq Admitted for theorems

100%

Correctness theorem stated

100%

Helper predicates defined

100%

Code ordering correct

83%

100%

Code comments present

100%

Semantic equivalence

100%

99%

-1%

Specifying a Merge Sort Algorithm

Informal requirements formalization

Criteria

Without context

With context

Theory block structure

100%

Function type signatures

100%

Sorted predicate defined

100%

Permutation/multiset predicate

100%

Precondition captured

100%

Postcondition captured

100%

Correctness theorem stated

100%

Proofs use sorry

100%

85%

Pattern matching used

100%

Code ordering correct

100%

Descriptive names used

100%

Comments present

100%

Standard library used

100%

Formalizing Number Theory Properties in Coq

Mathematical definition formalization in Coq

Criteria

Without context

With context

Coq imports present

100%

Nat type used

100%

Divisibility predicate defined

100%

Primality predicate defined

100%

GCD fixpoint defined

75%

100%

At least 3 theorems stated

100%

Theorems use Admitted

100%

Existential quantifier used

100%

Universal quantifier used

100%

Code ordering correct

100%

Comments present

100%

Simple definitions preferred

100%

Standard library used

100%

Repository: ArabelaTso/Skills-4-SE
Commit: 0f00a4f

Evaluated: 29 days ago
Agent: Claude Code
Model: Claude Sonnet 4.6

Table of Contents

Formalizing a Queue Data Structure Specifying a Merge Sort Algorithm Formalizing Number Theory Properties in Coq

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.