What does invariant-analyzer do?

Automatically infers loop invariants, verifies them against code, and generates a formal proof structure.

Which invariant patterns are supported?

Range, Accumulator, Pointer, and State invariants.

What outputs does it produce?

A success flag, a list of invariants, preconditions, postconditions, and a formal proof outline.

invariant-analyzer

npx machina-cli add skill a5c-ai/babysitter/invariant-analyzer --openclaw

Files (1)

SKILL.md

1.6 KB

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"]
}

Source

git clone https://github.com/a5c-ai/babysitter/blob/main/plugins/babysitter/skills/babysit/process/specializations/algorithms-optimization/skills/invariant-analyzer/SKILL.md

View on GitHub

Overview

Identifies and verifies loop invariants to support correctness proofs for algorithms. It can automatically infer invariants, verify them against code, extract pre/postconditions, and generate a formal proof structure. It also spots missing invariants to strengthen proofs.

How This Skill Works

Operates on the loop’s code using an invariant analysis framework that emphasizes Initialization, Maintenance, and Termination. It detects common invariant patterns—Range, Accumulator, Pointer, and State—infers candidate invariants, and validates them against the loop body, producing a structured proof outline.

When to Use It

Proving correctness during correctness-proof-testing of a new algorithm.
Verifying invariants against existing code during algorithm-implementation.
Learning and documenting loop invariants for unfamiliar code.
Handling range-based, accumulator-based, pointer-based, or state invariants.
Identifying missing invariants to strengthen formal proofs.

Quick Start

Step 1: Provide the loop code and specify the loopIndex.
Step 2: Run the analyzer to infer and verify invariants and extract pre/postconditions.
Step 3: Review the generated proofOutline and integrate into your correctness proof.

Best Practices

List Initialization, Maintenance, and Termination conditions clearly.
Start with common patterns (Range, Accumulator, Pointer, State) as templates.
Capture precise preconditions and postconditions alongside invariants.
Iteratively infer invariants and verify them against the loop body.
Document the proof steps, edge cases, and assumptions.

Example Use Cases

Proving a range loop invariant: for all i in [0, k), P(i) holds.
Verifying an accumulator invariant: the running sum equals sum of a[0..k-1].
Ensuring a pointer-based loop maintains a state invariant: left < right and processed elements satisfy a predicate.
Maintaining a state invariant within a data structure as operations modify it.
Identifying missing invariants in an algorithm's loop to strengthen the proof.

Frequently Asked Questions

Add this skill to your agents