OpenSkillIndex← back to search
claude-codescience

Babysitter smt-solver-interface

Interface with SMT solvers for verification and synthesis

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/smt-solver-interface" ~/.claude/skills/a5c-ai-babysitter-smt-solver-interface && rm -rf "$T"
manifest: library/specializations/domains/science/computer-science/skills/smt-solver-interface/SKILL.md
tags
#smt-solvers#formal-verification#logic-synthesis#z3#cvc5
source content

SMT Solver Interface

Purpose

Provides expert guidance on using SMT solvers for automated reasoning, verification, and program synthesis.

Capabilities

  • Z3 query generation
  • CVC5 interface
  • Theory selection guidance
  • Model extraction
  • Unsat core analysis
  • Incremental solving

Usage Guidelines

  1. Encoding: Encode problem in SMT-LIB format
  2. Theory Selection: Choose appropriate theories
  3. Solving: Run SMT solver
  4. Model Extraction: Extract satisfying assignments
  5. Debugging: Analyze unsat cores for debugging

Tools/Libraries

  • Z3
  • CVC5
  • Boolector
  • Yices