PDD is a methodology, and a tool, for changing code whose behavior you can't fully verify by reading it (legacy systems, or AI-generated code that passes review) without breaking it.
It recovers what the code actually does, locks that behavior in tests before changing it, and makes each change under gates that catch the case where the tests pass but the behavior is wrong. The gates are deterministic: a real exit code, not a model's opinion that the code looks fine. A gate either finds the gap or it doesn't.
The core check, pdd prove, grades the tests, not the code, so it keeps working as code generators improve: on a public SDK anyone can clone and re-run, one module reported 94% line coverage but a 0.68 mutation grade, green by coverage and unpinned in fact.
Code that passes every check and is still wrong. It has two causes:
- The tests pass but don't constrain the behavior. They would pass even if the code were wrong.
- An error is handled silently, so a broken system still looks healthy.
The gates address both.
| Move | What it does |
|---|---|
| MAP | Recover what the system actually does by reading the code (the names mislead). Produces a map of the system and its known traps. |
| PIN | Capture the current behavior in tests before any change. These characterization tests are the recovered spec. |
| CARVE | Split the work into review-sized units; prove the riskiest assumption first with a thin end-to-end spike. |
| SHIP | Make each change under mechanical gates: boundary cases, no-op paths, silent-failure checks. |
| PROVE | Show the behavior didn't change and the targeted debt is gone. Mutation confirms the tests would actually fail on a regression. |
Full rules: methodology/core.md.
The mechanical half of the methodology runs as a CLI with a real exit code you wire into pre-commit and CI. This is the part a model can't fake, and the part a stochastic "AI reviewer" structurally can't give you: a verdict that fails the build, not a summary that says it looks examined.
| Gate | Catches |
|---|---|
| no-op-paths | a conditional-cleanup method (prune / evict / expire …) with no test for the trigger-not-met path |
| boundary-tests | a comparison against a named threshold constant that no test even references by name |
| dead-branch | a comparison whose outcome is already decided by an earlier guard on the same variable |
| cover-the-mirror | a forward operation (open / acquire / subscribe …) whose inverse is missing |
| disposable-leak | a returned Disposable (onDid* / subscribe …) that is discarded |
| silent-failure | empty catches, swallowed promise rejections, and a catch whose whole body is a bare default escape (return null / [] / {} …) |
| vestigial | TODO / FIXME / TBD markers and not-implemented stubs |
| trace-requirements | a requirement id in the spec with no test that names it (opt-in) |
| pin-values | a test that asserts a type or truthiness instead of the value |
| cohesion | a file whose top-level symbols form two or more reference-disjoint clusters: several concerns sharing one module (TypeScript) |
| resource-leak | a discarded acquisition (open(p).write(x), bare Popen(...)) or a handle never closed and never handed off (Python) |
Each gate runs in one of three modes, set in a committed .pdd/config.yaml: block (a red verdict fails the run), warn (surfaced, non-blocking), or off. Most gates start as warn and earn block once their precision is proven on the codebase; no-op-paths ships as block, and trace-requirements ships off until a requirements spec is configured.
There are two kinds of gate: language-agnostic core gates (text), and language packs behind a JSON contract. TypeScript (ts-morph) and Python (libcst) packs ship today; a config declares one flow per language, and execution currently runs the first flow (multi-flow iteration is the next increment). Adding a language means implementing the contract; the core changes only by a dispatch-table row and the gates' language tags.
pdd prove is the oracle behind the proxy gates. It confirms a "covered" verdict by mutation: it flips the operator at a boundary, runs that constant's tests, and if nothing fails, the boundary was never actually pinned. pdd grade runs the same mutation check across a whole module; the public SDK above is unleash, an independent Apache-2.0 project, so that result is reproducible by anyone. Run against Cave, a ~3.4k-file TypeScript codebase and PDD's first dogfood target, it showed that of the 4 boundaries whose tests named the threshold constant, 3 were never checked at the == limit; a separate static gate flagged 10 of 14 threshold constants with no test naming them at all.
node cli/bin/pdd.ts init # scaffold .pdd/ (config + constitution) for a repo
node cli/bin/pdd.ts check # run the configured gates; non-zero exit on a blocking finding
node cli/bin/pdd.ts status # show the configured gates and modes
node cli/bin/pdd.ts prove # verify test-covered boundaries by mutation
node cli/bin/pdd.ts grade # mutation-grade a whole module: does coverage actually pin behavior
node cli/bin/pdd.ts map # the MAP pipeline: sweep → atlas → classify → carve (see --help)
node cli/bin/pdd.ts dashboard # read-only findings dashboard over .pdd/Needs Node 23.6+ (the CLI runs TypeScript source directly via Node's type-stripping). prove runs the target project's own test runner, so that project's dependencies must be installed. The Python pack gates need libcst on the interpreter PDD_PYTHON points at (default python3).
The same moves apply when an AI agent is doing the work. pdd/skills/ are Claude Code skills that trigger mid-task: recovering system truth (read-the-system, a footgun register, a silent-failure census, the system-truth atlas), locking behavior before a change (characterization tests, a reproducibility baseline), attention-sized decomposition, de-risk and decision gates, PR sizing, and test adequacy (boundary and no-op cases, properties, mutation grading).
claude plugin marketplace add AlexTavor/proof-driven-development
claude plugin install pdd@proof-driven-developmentpdd map → pdd roadmap (curate) → pdd roadmap signoff → pdd remediate → merge, re-map to reconcile
MAP produces a risk-ranked unit roadmap; you triage every unit at the gate (approve / deny / edit / split / refactor over an append-only ledger); sign-off freezes it and hands it to remediation, which fixes approved units in isolated worktrees under the same gates and commits them one-per-unit to a pdd/remediate branch for your review. Command-level truth (flags, artifacts, contracts, traps) lives in docs/reference.md.
People changing code they don't fully trust: maintaining or refactoring a legacy system, or reviewing and shipping AI-assisted changes where "tests pass" isn't enough.
Built and dogfooded: the methodology, the skills, and the gate CLI (init / status / check / prove / grade, the nine core gates above plus the TypeScript and Python pack gates, CI merge-gate wiring, and an opt-in pre-commit hook); the full MAP pipeline (pdd map: mechanical sweep → atlas → classify → carve into a risk-ranked unit roadmap); the human-in-the-loop roadmap gate (pdd roadmap: approve / deny / edit / move / split / refactor over an append-only ledger, plus sign-off) with its dashboard (pdd plan); a read-only findings dashboard (pdd dashboard); and the per-unit remediation loop (pdd remediate), today against mock fix providers. Planned: the real agent fix provider for remediate, and language packs beyond TypeScript and Python.
methodology/core.md: the rules.docs/reference.md: the operator reference: every command, artifact, and contract as the code actually behaves.- PDD explorer: an interactive map of the methodology, published at https://alextavor.github.io/pdd/ (source lives in the
alextavor.github.iorepo).