Individual skill

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.

skills/program-to-model-extractor/SKILL.md

Read pinned source

Source commit 4f38503747e0617504bce5329283ef837d375c09

What was checked

Matches the observed repository HEAD: Yes
Scanner rules are current: Yes
Repository scan complete: No
Skill scan complete: No
Observed behavior: Instructions only
Last checked: Nov 11, 2026

These are observations at the recorded commit, not a guarantee of safety. Review the source before running it.

Install this skill

Choose an agent in your Stack or copy a command below. Commands fetch the pinned commit and copy only this skill directory. Existing destinations are refused. Copying a command does not install anything.

An install command is unavailable: current rules, complete repository and skill scans, an eligible behavior level and a permitted license are required.

Repository context

Repository stars (not skill ratings): 260
Repository last updated: Aug 21, 2026
License: Apache-2.0

Observed agent integration: No specific integration evidence. Standard SKILL.md installation does not imply verified compatibility.

claude-skills Repository topic
metaprogramming Repository topic
software-development Repository topic
software-engineering Repository topic
claude Repository topic
claude-code Repository topic
data Derived category

Files and excerpt

File metadata and permitted, redacted excerpts come from the recorded scan. Source links are pinned to that commit.

Browse files

SKILL.mdcore · 6,230 bytes
SKILL.mdcore · 6,230 bytes
references/extraction_patterns.mddoc · 5,832 bytes
references/isabelle_syntax.mddoc · 4,619 bytes

Read excerpt


# Program-to-Model Extractor

Extract high-level mathematical models from functional code for formal reasoning in Isabelle/HOL.

## Overview

This skill transforms functional programs (Haskell, OCaml, F#) into abstract mathematical models suitable for formal verification in Isabelle/HOL. The extraction focuses on the algorithm's mathematical essence—capturing core properties, invariants, and structural patterns while abstracting away language-specific implementation details.

## Extraction Workflow

### 1. Analyze the Source Code

Identify key elements:
- **Data structures**: Algebraic types, lists, trees, custom types