OpenSkillIndex← back to search
claude-codescience

Babysitter model-checker-interface

Interface with multiple model checking tools for formal verification

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/model-checker-interface" ~/.claude/skills/a5c-ai-babysitter-model-checker-interface && rm -rf "$T"
manifest: library/specializations/domains/science/computer-science/skills/model-checker-interface/SKILL.md
tags
#formal-verification#model-checking#system-verification#spin-promela#nuxmv#uppaal
source content

Model Checker Interface

Purpose

Provides expert guidance on using model checking tools for formal verification of systems and protocols.

Capabilities

  • SPIN/Promela specification generation
  • NuSMV/NuXMV interface
  • UPPAAL for timed systems
  • Result parsing and visualization
  • Counterexample trace analysis
  • Abstraction refinement

Usage Guidelines

  1. Tool Selection: Choose appropriate model checker
  2. Specification: Translate system to checker's language
  3. Properties: Specify properties to verify
  4. Checking: Run model checker
  5. Analysis: Interpret results and counterexamples

Tools/Libraries

  • SPIN
  • NuSMV
  • UPPAAL
  • PRISM