OpenSkillIndex← back to search
claude-codescience

Babysitter loop-invariant-generator

Automatically generate and verify loop invariants for algorithm correctness proofs

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/loop-invariant-generator" ~/.claude/skills/a5c-ai-babysitter-loop-invariant-generator && rm -rf "$T"
manifest: library/specializations/domains/science/computer-science/skills/loop-invariant-generator/SKILL.md
tags
#loop-invariant#algorithm-proof#formal-verification#theorem-prover#code-analysis
source content

Loop Invariant Generator

Purpose

Provides expert guidance on generating and verifying loop invariants for algorithm correctness proofs using formal methods.

Capabilities

  • Infer candidate loop invariants from code structure
  • Verify initialization, maintenance, and termination conditions
  • Generate formal proof templates
  • Handle nested loops and complex data structures
  • Export to theorem provers (Dafny, Why3)
  • Suggest invariant strengthening

Usage Guidelines

  1. Code Analysis: Analyze loop structure and identify key properties
  2. Candidate Generation: Generate candidate invariants from code patterns
  3. Verification: Check initialization, maintenance, termination
  4. Strengthening: Refine invariants to prove desired properties
  5. Export: Generate proof obligations for theorem provers

Tools/Libraries

  • Dafny
  • Why3
  • SMT solvers (Z3, CVC5)
  • Static analysis frameworks