# Loop Invariant Generator

> Automatically generate and verify loop invariants for algorithm correctness proofs

- Skill: `a5c-ai/loop-invariant-generator` (Agent Skill)
- Install (CLI): `npx skillmds@latest add a5c-ai/loop-invariant-generator`
- Raw SKILL.md: https://api.skillmd.com/api/skills/a5c-ai/loop-invariant-generator/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/loop-invariant-generator

---


# 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