# Proof Obligation Registry

> Maintain durable proof-obligation registries with profile coverage and semantic ledgers

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

---


# Proof Obligation Registry

## Purpose

Extract, merge, and maintain a persistent proof state whose omissions and stale evidence are mechanically visible.

## Inputs

Problem statement, source artifact paths/hashes, optional draft, domain profile, optional prior registry, strictness, and run workspace.

## Procedure

1. Inventory definitions, quantified claims, external theorems, algorithms/reductions, complexity claims, and document references.
2. Assign stable IDs; merge prior records by ID and preserve history.
3. Build the hypothesis ledger and connect each use.
4. Build the use-site audit with exact substitutions, side conditions, signs, domains, and path tuples.
5. Instantiate every profile boundary row; require evidence or a reasoned N/A.
6. Populate random-distribution and convergence ledgers when expectations/limits occur.
7. Populate exact-arithmetic/bit-complexity rows for oracle or rational reductions.
8. Populate theorem-reference targets and uses.
9. For every selected module, populate each ledger named by `profile.requiredLedgers`, link at least one record to that module's applicable obligation, and close every such record before publication; an empty required ledger fails.
10. Mark uncertain records open; never self-certify them verified.
11. Run `python validators/validate_registry.py ...` as an `expectedExitCode: 0` shell gate; publication always uses `--strict publication`.

## Failure handling

- Missing source/hash: stop before extraction.
- Prior required ID removed: restore it as stale and trigger scope breakpoint.
- Rejection: append reason/history, reopen affected records, refine, and rerun validation.
- Unjustified N/A, unresolved dependency, or verified-without-evidence: hard failure.

## Output

Registry JSON, edge-matrix JSON, unresolved IDs, scope changes, and validation transcript. Agent prose cannot override the gate.