Agent-Skills.md

Agent Skills: SMT Solver Interface

Interface with SMT solvers for verification and synthesis

formal-verificationID: a5c-ai/babysitter/smt-solver-interface

Repository

a5c-ai/babysitter
a5c-aiLicense: MIT
244

Install this agent skill to your local

pnpm dlx add-skill https://github.com/a5c-ai/babysitter/tree/HEAD/plugins/babysitter/skills/babysit/process/specializations/domains/science/computer-science/skills/smt-solver-interface

Skill Files

Browse the full folder contents for smt-solver-interface.

Download Skill

Loading file tree…

plugins/babysitter/skills/babysit/process/specializations/domains/science/computer-science/skills/smt-solver-interface/SKILL.md

Skill Metadata

Name
smt-solver-interface
Description
Interface with SMT solvers for verification and synthesis

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