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]
According to GitHub Next, the workflow is:
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.
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.
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.
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.
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:
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.