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-extractor

What are skills?

Review — 86%

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/skill

Learn more

Validation — 11 / 11 Passed

Validation for skill structure

SKILL.md

Review

Evals

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%

Without context: $0.2867 · 2m 24s · 10 turns · 15 in / 6,688 out tokens

With context: $0.5780 · 3m 2s · 22 turns · 25 in / 7,513 out tokens

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%

Without context: $0.3880 · 2m 38s · 9 turns · 14 in / 10,019 out tokens

With context: $0.8553 · 5m 7s · 26 turns · 2,341 in / 14,721 out tokens

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%

Without context: $0.4172 · 3m 4s · 13 turns · 68 in / 10,070 out tokens

With context: $0.5233 · 2m 49s · 15 turns · 19 in / 8,851 out tokens

Evaluated: about 13 hours ago
Agent: Claude Code

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.