Individual skill

refinement-step-generator

Generate systematic refinement steps from high-level specifications to concrete implementations in Isabelle/HOL or Coq, preserving correctness obligations at each step. Use when working with formal verification, program refinement, proof development, or when translating abstract specifications into executable code while maintaining formal guarantees. Supports data refinement (abstract types → concrete structures), algorithmic refinement (specifications → algorithms), and stepwise refinement with proof obligations.

skills/refinement-step-generator/SKILL.md

Read pinned source

Source commit 4f38503747e0617504bce5329283ef837d375c09

What was checked

Matches the observed repository HEAD: Yes
Scanner rules are current: No
Repository scan complete: No
Skill scan complete: Yes
Observed behavior: Not checked yet
Last checked: Nov 6, 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 · 9,252 bytes
references/coq_refinement.mddoc · 11,062 bytes
references/isabelle_refinement.mddoc · 9,707 bytes
references/refinement_patterns.mddoc · 10,144 bytes

Read excerpt


# Refinement Step Generator

Generate systematic refinement steps that transform high-level specifications into concrete, executable implementations while preserving correctness through formal proofs.

## Overview

Refinement is the process of transforming abstract specifications into concrete implementations through a series of correctness-preserving steps. Each refinement step:

1. Makes the specification more concrete (closer to executable code)
2. Preserves correctness through formal proof obligations
3. Maintains a clear abstraction relation between levels
4. Can be verified independently

This skill provides guidance for generating refinement steps in Isabelle/HOL and Coq.