Babysitter invariant-analyzer

Identify and verify loop invariants for 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/algorithms-optimization/skills/invariant-analyzer" ~/.claude/skills/a5c-ai-babysitter-invariant-analyzer && rm -rf "$T"

manifest: library/specializations/algorithms-optimization/skills/invariant-analyzer/SKILL.md

Invariant Analyzer Skill

Purpose

Identify and verify loop invariants to help construct correctness proofs for algorithms.

Capabilities

Automatic loop invariant inference
Invariant verification against code
Precondition/postcondition extraction
Generate formal proof structure
Identify missing invariants

Target Processes

correctness-proof-testing
algorithm-implementation

Invariant Analysis Framework

Loop Invariant Properties

Initialization: True before first iteration
Maintenance: If true before iteration, true after
Termination: Provides useful property at end

Common Invariant Patterns

Range invariants: "for all i in [0, k), property P(i) holds"
Accumulator invariants: "sum equals sum of a[0..k-1]"
Pointer invariants: "left < right and all elements < left are processed"
State invariants: "data structure maintains property X"

Input Schema

{
  "type": "object",
  "properties": {
    "code": { "type": "string" },
    "language": { "type": "string" },
    "loopIndex": { "type": "integer" },
    "expectedInvariant": { "type": "string" }
  },
  "required": ["code"]
}

Output Schema

{
  "type": "object",
  "properties": {
    "success": { "type": "boolean" },
    "invariants": { "type": "array" },
    "preconditions": { "type": "array" },
    "postconditions": { "type": "array" },
    "proofOutline": { "type": "string" }
  },
  "required": ["success"]
}