· · Matthew Ford · 4 min read
Proof-driven development: what GitHub’s PDD Kit changes and what it doesn’t
GitHub's latest agent announcement has a bold promise: instead of reviewing every line your agent writes, approve a specification and let a verifier prove the code meets it.
It is a good idea. It is also much narrower than the headline suggests.
The Proof-Driven Development Kit, or PDD Kit, is a research preview from GitHub Next and Microsoft Research. The announcement describes a workflow where a plan becomes a formal Verus specification, the Verus verifier proves that agent-generated Rust code meets that specification for every input, and the result becomes a verified pull request.[4] GitHub says the combination of Chopin and PDD Kit could let teams ship AI-generated code without line-by-line review, with stronger assurance than code review and testing alone.[5]
What PDD Kit actually does
According to GitHub Next, the workflow is:
- start with a plan;
- infer intent and propose a formal Verus specification;
- ask a human to approve that specification;
- use the verifier to prove the generated code meets it;
- fall back to tests and computer-use agents where proof is not possible.[4]
It works on Rust today. There is no announced support for TypeScript, Python or Ruby, so this is not a general answer for every application stack.
This is not test-driven development with a fancier name
A test shows what happens for selected inputs. A proof covers every input allowed by the specification.
That makes the specification the thing you really need to get right. "The login should be secure" will not help. A stronger specification would say which credentials are accepted, how attempts are limited, what state changes are allowed and which behaviour must never occur.
The work of defining intent has not disappeared. It has become more visible, and more demanding.
Where Spec Kit and Chopin fit
GitHub's Spec Kit is separate. It is an open-source toolkit for giving coding agents structured processes, reusable templates and documented outcomes.[3]
Chopin is GitHub Next's research prototype for multiplayer agentic planning. People and agents can work on plans organised around GitHub repositories.[2]
PDD Kit sits further along the verification path. Spec Kit helps structure the work. Chopin helps people and agents plan together. PDD Kit attempts to prove that a subset of the resulting code satisfies a formal specification.
What a proof cannot tell you
A proof is only as useful as the specification and the boundary around it.
It does not prove that the product requirement was the right one, that the specification captured every business rule, that the surrounding infrastructure is safe or that third-party services will behave as expected. It also does not cover code outside the supported language and proof scope.
Where proof is not possible, the announced fallback is empirical verification with tests and computer-use agents.[4] That fallback still needs engineering discipline. "The agent tried it and it worked" is not an evaluation.
Use more than one kind of control
A Microsoft Research/CMU benchmark makes the broader review problem clear. The best code-review agent configuration caught 71.9% of human-verified bugs within its top-five comments, up from 47.7% five months earlier. The same research found that agents still missed more than 20% of bugs humans found, with performance dropping on proprietary repositories that required more project context.[1]
That points to a mixed approach:
- precise specifications where behaviour can be formalised;
- proofs for properties that can be verified;
- tests and static checks for broader behaviour;
- independent review for context-heavy changes;
- staged deployment and rollback for production risk;
- human approval where the blast radius justifies it.
What to do before PDD Kit is generally available
You do not need to wait for this tool to get value from the idea.
Start by separating provable code from behavioural code. Parsers, validators, state machines, permission rules and data transformations are better candidates for formal contracts than broad UI or workflow behaviour.
Then write reviewable intent before implementation. A specification should name allowed inputs, required outputs, invariants and unacceptable actions.
Then define the evidence gate. Decide which combination of proofs, tests, review, deployment controls and production monitoring is required before an agent-generated change can ship.
PDD Kit is worth watching because it brings formal verification into an agent workflow. It is not worth treating as a reason to skip specification work or human judgement. Those are exactly the parts that determine whether the proof means anything.
Our AI consulting and automation service helps teams define those boundaries, evaluation gates and delivery workflows.
Sources
Discuss your software, technical leadership or AI plans
Tell us what you need to build, improve or decide.
We can help with software development and ongoing support, fractional CTO leadership, and practical AI adoption. Speak to our senior team about your priorities, our approach and availability.
