Proof Obligations banner
ekirton ekirton

Proof Obligations

Development community

Description

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

Installation

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.

Full documentation available on GitHub

View Source Repository