# DAG > Persistent axiom registry + formal proof prompt builder. Transforms any project into a DAG-structured knowledge base where every conclusion cites parent axioms and inference rules. Axioms co-built with user, saved to .dag/ files, referenced by ID (A1, T1, D1, H1) to save tokens and prevent drift. Use when user says "/dag", "/dag init", "/dag prove", "/dag derive", "formal proof mode", or wants tr… - **Type:** Skill - **Install:** `agentstack add skill-ndpvt-web-claude-dag-skill-claude-dag-skill` - **Verified:** Yes — security-reviewed for prompt injection and unsafe behavior - **Seller:** [ndpvt-web](https://agentstack.voostack.com/s/ndpvt-web) - **Installs:** 0 - **Category:** [Agent Skills](https://agentstack.voostack.com/c/agent-skills) - **Latest version:** 0.1.0 - **License:** MIT - **Upstream author:** [ndpvt-web](https://github.com/ndpvt-web) - **Source:** https://github.com/ndpvt-web/claude-dag-skill ## Install ```sh agentstack add skill-ndpvt-web-claude-dag-skill-claude-dag-skill ``` Requires the [AgentStack CLI](https://agentstack.voostack.com/docs/cli). Works with Claude Code, Cursor, and any MCP-compatible agent. ## About # DAG — Persistent Axiom Registry + Formal Proof Builder Every project gets a `.dag/` directory. Axioms live there. Future proofs reference by ID — not re-stated. Nothing drifts. Everything traces. ## Caveman Rules (all prose output from this skill) Drop: "I would like to", "please note", "it's worth mentioning", "in order to" Use fragments. "No session store. JWT only." not "You should not use a session store." Keep exact: code, IDs, field names, inference rules, statements — never compressed. Target: 50-65% fewer tokens on prose. Technical accuracy: unchanged. ## Registry Structure ``` {project-root}/ .dag/ registry/ axioms/ # A-type: structural ground truths (non-derivable) A1.md A2.md ... definitions/ # D-type: what terms mean D1.md D2.md ... hypotheses/ # H-type: scope/existence claims (empirical, falsifiable) H1.md H2.md ... theorems/ # T-type: derived conclusions with proof chains T1.md T2.md ... deprecated/ # Tombstones: superseded entries, never deleted A2.md ... meta/ registry.json # Machine index + consistency state + file paths provenance.json # Full derivation graph sessions/ YYYY-MM-DD-N.md # Per-session typed scratchpads ``` One file per entry. Each file = one atom. `registry.json` is the index: ID → file path + one-liner + status + deps. Agent loads only the files it needs — never more. ## Why Directories, Not Files The three Aristotelian types fail differently: - D-type: term meaning shifts (drift) → audited separately - H-type: world changes, scope assumptions go stale → each needs falsification criterion - A-type: can contradict each other → write-time contradiction check on every add - T-type: derived conclusions — stay theorems permanently; if content needs to become foundational, human writes a new A-type from scratch Each type lives in its own directory. Each entry lives in its own file. Retrieval cost = one file read per entry, not one file read per type. This is the atomic access guarantee. ## ID Scheme | Prefix | Type | Example | |--------|------|---------| | D | Definition | D1, D2 | | H | Hypothesis | H1, H2 | | A | Axiom | A1, A2 | | T | Theorem | T1, T2 | IDs are permanent. Never reused after deprecation. Deprecated entries get tombstones written to `registry/deprecated/{original-ID}.md`. ## Entry Format Every entry has universal mandatory fields: ```yaml --- id: A3 type: axiom label: "short-human-name" statement: "The full formal statement. One sentence. No ambiguity." created: YYYY-MM-DD created_by: human # human | derived status: active # active | deprecated | under-review --- ``` Type-specific additional fields — see references/registry-spec.md. **Mandatory rules:** - A-type: `rationale` field required. Cannot be empty. Axiom without rationale = hypothesis in disguise. - T-type: `derived_from` field required. Theorem without provenance = orphaned claim. - H-type: `falsification` field required. Hypothesis without falsification = belief, not science. ## Commands | Command | What it does | |---------|-------------| | `/dag init` | Bootstrapping — co-build registry with user (see Bootstrapping section) | | `/dag prove [claim]` | Build formal proof chain against registry | | `/dag derive [claim] from [IDs]` | Add new theorem after 5-check validation | | `/dag add axiom` | Add A-type after contradiction check + derivability probe | | `/dag add definition` | Add D-type; flags dependent axioms as under-review | | `/dag add hypothesis` | Add H-type with mandatory falsification criterion | | `/dag review [H-ID]` | Review an H-type entry — log verdict (valid / amended / deprecated), reset staleness clock | | `/dag deprecate [ID]` | Deprecate entry; creates tombstone; checks downstream theorems first | | `/dag status` | Consistency report from registry.json | | `/dag audit` | Full consistency re-check, all entries | | `/dag session` | Print current session scratchpad | ## Workflow 1: First Run — `/dag init` Check `.dag/registry/axioms/` directory first. If `.md` files exist → load `registry.json` for summary, ask: continue / review / start fresh. Never silently overwrite. Then run bootstrapping in strict order (definitions → hypotheses → axioms). See references/bootstrapping.md for full dialogue. **Phase order is mandatory.** You cannot write a well-formed axiom before fixing the meaning of the terms it uses. **Key rule during bootstrapping:** For every proposed axiom, run the derivability probe: > "Could this be derived from the definitions and hypotheses you've already stated, plus common knowledge?" If yes → it's a theorem candidate, not an axiom. Derive it, add as T-type. If no → write it as A-type with a mandatory rationale. **Completeness checks (qualitative — no fixed counts):** - Definitions: have you named every project-specific term that could mean different things to different people? If any axiom uses a term someone could reasonably misread, it needs a definition. - Hypotheses: have you made explicit every assumption about the world that, if false, would change your conclusions? - Axioms: is every entry genuinely non-derivable from existing entries plus common knowledge? The minimum sufficient set is the goal — neither too few (gaps in reasoning) nor inflated (n² contradiction surface). After bootstrapping, write all entry files atomically — one file per entry in its type directory (`registry/definitions/D1.md`, `registry/axioms/A1.md`, etc.). Update `registry.json` last, after every entry file exists. Print summary: ``` Registry initialized for [project]: N definitions (D1-DN) N hypotheses (H1-HN) N axioms (A1-AN) 0 theorems Consistency: CLEAN ``` ## Workflow 2: Proof Chain — `/dag prove [claim]` **The LLM is the translator. The registry is the verifier.** The LLM does not generate truths. It translates the claim into derivation steps that cite registry IDs. Steps that cannot cite a registry ID must be flagged — not resolved silently. **Session system prompt for every proof chain:** > "You are constructing a derivation, not generating a position. Every step must cite a specific registry ID. Steps that cannot cite a registry ID must be flagged as HIDDEN ASSUMPTION. Do not resolve hidden assumptions — surface them." **Proof output format (always):** ``` AXIOM LAYER (active entries used) ─────────────────────────────────────────────────────── A1: [statement] [active] D2: [statement] [active] THEOREM LAYER ─────────────────────────────────────────────────────── T_new: [conclusion] because: A1, D2 rule: modus ponens confidence: CERTAIN | PROBABLE | UNCERTAIN therefore: [concrete decision] HIDDEN ASSUMPTIONS SURFACED ─────────────────────────────────────────────────────── [HIDDEN ASSUMPTION] [text] → Candidate H-type entry VERIFICATION ─────────────────────────────────────────────────────── [check] [decision] traces to [ID] [X] [decision] NO PARENT → MISSING AXIOM: [what would justify this] PROOF CONFIDENCE SUMMARY ─────────────────────────────────────────────────────── [CERTAIN N] [PROBABLE N] [UNCERTAIN N] Weakest link: [step with lowest confidence + reason] ``` **Confidence band definitions (mandatory per proof step):** | Band | Meaning | When to assign | |------|---------|----------------| | CERTAIN | Direct logical consequence; no assumptions beyond stated premises; formal rule applies cleanly | Modus ponens / transitivity where premise-to-conclusion match is unambiguous | | PROBABLE | Follows with standard domain reasoning; requires one unstated assumption that is common knowledge or industry standard | Step needs a bridging premise not in registry — flag it as [HIDDEN ASSUMPTION] candidate | | UNCERTAIN | Logical gap present; cannot close without adding an H-type or A-type entry; the step may be wrong | Premises do not entail conclusion without additional claims that are NOT common knowledge | **Confidence rules:** - A proof chain where ALL steps are CERTAIN → can be written as T-type without qualification - A proof chain with PROBABLE steps → can be written as T-type IF all PROBABLE steps have their hidden assumption flagged and user confirms - A proof chain with ANY UNCERTAIN step → BLOCK write. Must add missing H-type or A-type entry first, then re-derive - The proof confidence summary is mandatory at the end of every /dag prove or /dag derive output After proof: ask "Should any hidden assumptions be added as H-type entries?" ## Workflow 3: Add Theorem — `/dag derive [claim] from [IDs]` Five checks before writing a new theorem entry file: 1. **Premise existence**: all cited IDs exist and are `status: active` 2. **Term consistency**: all terms in statement have D-type definitions or are general language 3. **Inference validity**: LLM evaluates whether claim follows from premises. Hidden assumptions surfaced as H-type candidates, not silently absorbed. 4. **Contradiction check**: new theorem checked against all active entries (see references/failure-modes.md for check prompt) 5. **Loop check**: no circular dependencies in `derived_from` chain If check 3 surfaces hidden assumptions → pause. Ask: "Add as H-type entry or revise derivation?" Do not write theorem until resolved. ## Workflow 4: Session Scratchpad Every session creates `.dag/sessions/YYYY-MM-DD-N.md`. All working claims are typed: ```markdown [AXIOM-REF A3] statement cited from registry [HYPOTHESIS-REF H1] statement cited from registry [ASSUMPTION] unstated assumption — candidate H-type [DERIVED] conclusion with cited IDs [CONTRADICTION FLAG] conflict with [IDs] — requires resolution [THEOREM CANDIDATE] T_n: candidate for /dag derive [QUESTION] open question ``` No untagged entries in the formal scratchpad section. ## Token Load Modes **Mode 1 — Summary Index (default):** Read `registry.json` entry_index — one-liner + status + file path per entry. Use at session start, for scoping. Never load individual entry files in this mode. **Mode 2 — Targeted Full Load (during active proof):** Read the individual entry file for each cited ID using the `file` path from `registry.json`. Load only what the current proof step actually cites — nothing more. Example: `Read .dag/registry/axioms/A3.md` to get A3's full text — nothing else loads. **Mode 3 — Full Registry Load:** Only for: /dag init, /dag audit, /dag deprecate. Read all individual entry files across all type directories. Never for routine proof chains. **Load decision:** - Session start → Mode 1 (registry.json only) - /dag prove or /dag derive → Mode 1 + Read individual entry files on demand (Mode 2) - /dag status → Read registry.json only (no entry file loads) - /dag init / audit / deprecate → Mode 3 (all entry files) **Why this works:** An agent reading A3 does `Read .dag/registry/axioms/A3.md`. It loads only A3. Under the old format, getting A3 required reading axioms.md — loading every other axiom with it. Individual files = atomic access = zero context pollution. ## What This Skill Must NOT Do - Auto-generate axioms without human confirmation of each - Silently absorb hidden assumptions surfaced during proof chains - Delete any entry without creating a tombstone - Add theorem without `derived_from` field - Add axiom without `rationale` field - Promote theorems to axioms mechanically — if a theorem's content needs to be foundational, the human writes a NEW A-type entry from scratch with their own words; do not copy-promote - Load Mode 3 for routine proof chains - Re-use deprecated IDs ## References - **Entry format specs + example registry**: references/registry-spec.md - **Bootstrapping dialogue in full**: references/bootstrapping.md - **Failure mode guards + contradiction check prompt**: references/failure-modes.md ## Source & license This open-source skill is cataloged on AgentStack and links to its original source — we do not rehost the code. - **Author:** [ndpvt-web](https://github.com/ndpvt-web) - **Source:** [ndpvt-web/claude-dag-skill](https://github.com/ndpvt-web/claude-dag-skill) - **License:** MIT Install and usage instructions live in the source repository linked above. ## Pricing - **Free** — Free ## Security capabilities Automated source analysis of v0.1.0 — what this tool can access: - **Network access:** no - **Filesystem access:** no - **Shell / process execution:** no - **Environment & secrets:** no - **Dynamic code execution:** no *"Yes" means the capability is present in the source — more access means more to trust, not that it is unsafe.* ## Versions - **0.1.0** — security scan: passed — Imported from the upstream source. ## Links - Listing page: https://agentstack.voostack.com/l/skill-ndpvt-web-claude-dag-skill-claude-dag-skill - Seller: https://agentstack.voostack.com/s/ndpvt-web - Browse the marketplace: https://agentstack.voostack.com/browse --- Listed on AgentStack — the marketplace for AI agent skills and MCP servers. Every listing is security-reviewed. Creators keep 70%.