# Invariant Analyzer

> Identify and verify loop invariants for correctness proofs

- Skill: `a5c-ai/invariant-analyzer` (Agent Skill, multi-file: 2 files)
- Install (CLI): `npx skillmds@latest add a5c-ai/invariant-analyzer`
- Raw SKILL.md: https://api.skillmd.com/api/skills/a5c-ai/invariant-analyzer/raw
- Safety review: pending (external: skill-scanner PASS, skillspector PASS)
- Works with: Claude Code, Claude.ai, OpenAI Codex
- Category: Coding & Dev Tools
- Author: a5c-ai (https://skillmd.com/u/a5c-ai)
- Updated: 2026-09-09
- Page: https://skillmd.com/skills/a5c-ai/invariant-analyzer

---


# 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
1. **Initialization**: True before first iteration
2. **Maintenance**: If true before iteration, true after
3. **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

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

## Output Schema

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