# Termination Analyzer

> Prove termination of algorithms and programs using ranking functions and well-founded orderings

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

---


# Termination Analyzer

## Purpose

Provides expert guidance on proving termination of algorithms through ranking functions, well-founded orderings, and automated analysis.

## Capabilities

- Identify ranking/variant functions automatically
- Prove well-founded orderings
- Handle mutual recursion
- Detect potential non-termination
- Generate termination certificates
- Analyze complex control flow

## Usage Guidelines

1. **Structure Analysis**: Identify recursive calls and loop structures
2. **Ranking Function**: Find or construct appropriate ranking function
3. **Ordering Proof**: Prove well-foundedness of the ordering
4. **Certificate Generation**: Generate formal termination proof
5. **Non-termination Detection**: Flag potential infinite loops

## Tools/Libraries

- AProVE
- T2
- Ultimate Automizer
- SMT solvers