refinement-step-generator
From the author
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.
Install
npx skills add ArabelaTso/Skills-4-SE --skill refinement-step-generator -a claude-code
Installs to .claude/skills/refinement-step-generator/ · Each command fetches the skill straight from GitHub with the open skills CLI.
Byte-identical to the scanned commit, with the repository’s licence and a SOURCE.txt.
Want your agent to suggest skills while you type? See how to use skills from your IDE.
Safety checks on SKILL.md
No warnings.
Why 83
aiqbench computes the trust score from public signals. It is not a security audit, so read a skill before you install it.
Similar skills
Closest to this one by what they do and when they are used.
- formal-spec-generatorArabelaTso/Skills-4-SEGenerate 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.Planning★ 258
- proof-skeleton-generatorArabelaTso/Skills-4-SEGenerate structured proof skeletons with tactics, strategies, and intermediate lemmas for theorems in Isabelle/HOL or Coq. Use when users need to: (1) Create proof outlines for theorem statements, (2) Generate proof structure with tactic placeholders, (3) Identify key lemmas needed for a proof, (4) Plan proof strategies (induction, case analysis, forward/backward reasoning), (5) Scaffold proofs with intermediate steps and subgoals, or (6) Convert theorem statements into detailed proof templates. Supports both Isabelle/HOL and Coq equally.Planning★ 258
- proof-carrying-code-generatorArabelaTso/Skills-4-SEGenerate executable code together with formal proofs certifying safety and correctness properties in Isabelle/HOL or Coq. Use when building verified software, safety-critical systems, or when formal guarantees are required. Produces code with accompanying proofs for memory safety, bounds checking, functional correctness, invariant preservation, and termination. Supports extraction to OCaml/Haskell/SML and integration with existing codebases.Engineering★ 258
- specification-generatorArabelaTso/Skills-4-SEGenerate formal specifications including preconditions, postconditions, invariants, and contracts from code or requirements. Use this skill when documenting APIs, creating formal verification annotations, defining function contracts, specifying class invariants, writing design-by-contract code, or preparing code for formal verification. Supports multiple specification languages including JML, ACSL, Dafny, Eiffel contracts, and documentation annotations.Planning★ 258
- requirement-enhancerArabelaTso/Skills-4-SEIteratively enhance user requirements into clear, complete, actionable specifications through analysis and clarification. Use when: (1) Users provide initial requirements that need refinement, (2) Requirements are vague, incomplete, or ambiguous, (3) Creating formal specifications from informal descriptions, (4) Identifying missing constraints, edge cases, or acceptance criteria, (5) Clarifying assumptions and implicit dependencies, or (6) Preparing requirements for design, implementation, or verification. Operates interactively: analyze → ask clarifying questions → refine based on responses.Planning★ 258
- code-reviewflutter/agent-pluginsPerforms a comprehensive, multi-step code review of pull requests or local code changes, using iterative refinement (generation, critique, synthesis) to ensure high-quality, actionable feedback. Use when you need to review code changes thoroughly.OfficialEngineering★ 3.1K
Ratings & reviews
—
no reviews
Tried this skill? Rate it to help others. Sign in
Discussion
Join the discussion. Sign in