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.

1.11x

Quality

86%

Does it follow best practices?

Impact

98%

1.11x

Average score across 3 eval scenarios

Securityby

Passed

No known issues

Evaluation results

100%

Formal Model Extraction: Insertion Sort

Sorting algorithm Isabelle extraction

Criteria

Without context

With context

fun for insert

100%

fun for sort

100%

linorder type class

100%

sorted predicate

100%

mset permutation lemma

100%

Combined correctness lemma

100%

Grouped lemmas

100%

No performance details

100%

No comparison count

100%

Mathematical names

100%

Abstraction comment

100%

List cons syntax

100%

23%

Formal Model Extraction: Number Theory Utilities

Tail recursion and general recursion modeling

Criteria

Without context

With context

fun for sum_acc

50%

100%

Accumulator correctness lemma

100%

fun for factorial_aux

100%

function for gcd

16%

100%

pat_completeness for gcd

100%

Explicit termination measure

91%

100%

No stack annotations

100%

Mathematical names

100%

Grouped lemmas per function

100%

GCD correctness lemma

100%

definition for simple non-recursive

100%

Choice explanation comments

100%

94%

Formal Model Extraction: Binary Search Tree Operations

Tree datatypes and option type modeling

Criteria

Without context

With context

datatype declaration

100%

Leaf and Node constructors

100%

fun for insert

100%

fun for member

100%

option type for find_min

100%

case analysis for option

37%

25%

chain/bind modeled

100%

Grouped tree lemmas

100%

Mathematical property lemmas

100%

No implementation details

100%

Mathematical names

100%

Option type note

100%

No duplicate insertion

100%

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

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

Table of Contents

Formal Model Extraction: Insertion Sort Formal Model Extraction: Number Theory Utilities Formal Model Extraction: Binary Search Tree Operations

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.