OpenSkillIndex← back to search
claude-codescience

Babysitter counterexample-guided-refinement

Implement CEGAR for synthesis and verification workflows

install
source · Clone the upstream repo
git clone https://github.com/a5c-ai/babysitter
Claude Code · Install into ~/.claude/skills/
T=$(mktemp -d) && git clone --depth=1 https://github.com/a5c-ai/babysitter "$T" && mkdir -p ~/.claude/skills && cp -r "$T/library/specializations/domains/science/computer-science/skills/counterexample-guided-refinement" ~/.claude/skills/a5c-ai-babysitter-counterexample-guided-refinement && rm -rf "$T"
manifest: library/specializations/domains/science/computer-science/skills/counterexample-guided-refinement/SKILL.md
tags
#verification#program-synthesis#abstraction-refinement#cegar#formal-methods
source content

Counterexample-Guided Refinement

Purpose

Provides expert guidance on CEGAR (Counterexample-Guided Abstraction Refinement) for verification and synthesis.

Capabilities

  • Counterexample analysis
  • Predicate abstraction refinement
  • Interpolation-based refinement
  • Abstraction refinement loop management
  • Convergence analysis
  • Spurious counterexample detection

Usage Guidelines

  1. Initial Abstraction: Define initial abstraction
  2. Verification: Check abstract model
  3. Counterexample Analysis: Analyze counterexamples
  4. Refinement: Refine abstraction if spurious
  5. Iteration: Repeat until verified or real counterexample

Tools/Libraries

  • CPAChecker
  • SeaHorn
  • BLAST
  • SLAM