ekirton

Proof Obligations — Development skill for Claude Code

Development community

Scan the entire Coq project for proof obligations (admit, Admitted, Axiom declarations), classify each by intent, rank by severity, and produce a structured summary report.

How to install Proof Obligations

Installs to ~/.claude/skills/ekirton-poule-proof-obligations/SKILL.md

Terminal

mkdir -p ~/.claude/skills/ekirton-poule-proof-obligations && curl -fsSL https://raw.githubusercontent.com/ekirton/Poule/HEAD/commands/proof-obligations.md -o ~/.claude/skills/ekirton-poule-proof-obligations/SKILL.md

Restart Claude Code, or start a new session, for it to be picked up.

What Proof Obligations does

Scan the entire Coq project for proof obligations (`admit`, `Admitted`, `Axiom` declarations), classify each by intent, rank by severity, and produce a structured summary report. This command is read-only — it never modifies source files.

Step 1: Discover `.v` files

Use Glob with `**/*.v` to find all Coq source files in the project. If no `.v` files are found, report "No Coq source files found in this project" and stop.

Step 2: Scan for obligations

Use Grep to search all `.v` files for

Alternatives in Development

Axiom — Battle-tested Claude Code skills for modern xOS (iOS, iPadOS, watchOS, tvOS) development with 13 production-re 2.6k ★
Axiom Marketplace Submission Guide — Axiom Marketplace Submission Guide skill 834 ★
Translate Book — Claude Code skill that translates entire books (PDF/DOCX/EPUB) into any language using parallel subagents 542 ★