Yesterday GitHub Next and Microsoft Research announced the Proof-Driven Development Kit (PDD Kit), now in research preview. The pitch, in GitHub Next's own words: "How do you guarantee your agent's code is correct? You prove it." Instead of a human reading an agent-generated diff line by line, a verifier reads a formal specification and checks the code against it for every input. I spend most of my time making coding agents behave inside config rules, so a tool that moves trust from "I read the diff" to "the spec checked the code" is exactly my kind of news. Here is what the kit actually does, the research it sits on, and the three places it stops working.
What the PDD Kit actually does
The workflow GitHub Next laid out, using a sample login flow, runs in five steps:
- Plan. A team plans the feature together inside Chopin, GitHub Next's multiplayer agentic planning tool.
- Spec. PDD Kit discusses the code, infers intent, and proposes a formal specification written in Verus, an existing open-source proof language for Rust.
- Approve. A human approves the spec, not the code.
- Prove. The Verus verifier automatically proves the agent's generated code satisfies that spec for every input.
- Fallback. Where a full proof is not possible, the kit falls back to tests and computer-use agents for empirical checking.
The end product is a verified pull request. GitHub's own framing of the stakes: Chopin plus PDD Kit "enable teams to ship AI-generated code to production without reviewing it line by line, with stronger assurance than code review and testing alone." That is a vendor describing its own research preview, not an audited result, so hold the claim loosely.
The spec is the artifact you review
The interesting inversion is what the human actually looks at. You review a specification, and the machine reviews the implementation against it. In Verus, a spec annotates functions with preconditions and postconditions the verifier must discharge. Simplified to show the shape:
verus! {
spec fn max_attempts() -> nat { 5 }
fn check_attempt(failed: nat) -> (allowed: bool)
ensures allowed == (failed < max_attempts())
{
failed < max_attempts()
}
}
The verifier does not run this code on test cases. It proves the relationship holds for every possible input, which is a different and much stronger guarantee than a green test suite. The cost is that someone has to write, or in this case approve, a spec precise enough to be provable. Vague requirements make for unprovable specs, and that burden does not disappear, it moves to the spec review.
The research underneath: AutoVerus and VeruSAGE
PDD Kit is not a verifier built from scratch. Verus is a separate, established proof framework for Rust, and Microsoft Research's verus-proof-synthesis repository shows the groundwork: two LLM-driven systems, AutoVerus and VeruSAGE, that generate and repair Verus proofs. They were benchmarked against 150 and 849 verification tasks respectively. What PDD Kit appears to add is packaging: the first time that proof-synthesis research line has been folded into a planning-to-PR product workflow rather than a benchmark exercise.
Where the proofs stop
Three limits matter more than the feature list.
Rust only. Verus checks Rust. GitHub Next says the kit "works on Rust today," with no new language and no change to how you produce the code. If your agents write TypeScript or Python, there is nothing to install yet.
Only what a spec can express. Formal proof covers properties you can state precisely: input/output contracts, invariants, state machine transitions. UI behavior, most I/O-heavy logic, and anything where "correct" is a judgment rather than a property still needs the fallback path of tests and human review. That fallback is exactly where today's review burden already lives.
Research preview status. Chopin, the planning environment this depends on, is listed on GitHub Next's projects page as a research prototype dated September 2026. GitHub Next has a track record of prototypes, Repo Mind, Project Copernicus, SpecLang among them, that never reached general availability. The first public demo against real code is at GitHub Universe, October 28-29, 2026.
What this means for your agent rules
The practical takeaway is not "wait for GA." It is that the durable split in an agent-heavy codebase is between provable and not-provable code, and your config should already know which is which.
Parsers, state machines, and data-structure invariants are provable territory, with or without PDD Kit, because Verus is open source and usable today. Most front-end work is not. Your rules files still decide what the agent attempts and how it verifies itself in the non-provable majority, which is why I keep the enforcement placement question (config files versus hooks) separate from the verification question. Proof narrows the slice of code that needs human eyes. It does not remove the need to tell the agent what "done" means.
What I would do before any GA
Three things hold value regardless of whether PDD Kit ships.
- Sort your codebase into provable and not-provable. Contracts with clear inputs and outputs on one side, everything behavioral on the other. This is useful inventory even if you never write a spec.
- Try Verus standalone on one pure function. The toolchain is MIT-licensed and independent of GitHub's preview. One afternoon with a small function teaches you what a spec costs to write.
- Watch the Universe demo. The Speakeasy session on October 28-29 is the first chance to see the spec-approval and proof steps run against real code rather than an announcement thread.
The fallback path is still on you
The quiet part of the announcement is step five. Where proofs are impossible, PDD Kit falls back to tests and computer-use agents, which is what you are already doing. The discipline that pays off there is the same one I run on every agent task: decide what evidence counts as done before the agent starts, gate the merge on that evidence, and never let "the agent said it works" pass as verification. The agent anti-patterns I keep hitting are mostly failures to define done.
Proof-driven development is the strongest answer I have seen to the review bottleneck, and it is honest about only covering part of the problem. For the rest, the spec you owe your agent is a rules file that says what verified means.
Top comments (1)
Step 3 is the real inversion here — reviewing the spec instead of the diff. One caution from the Verus side: proof effort scales with how stateful the code is, so parsers and data-structure invariants are the sweet spot, while anything doing async I/O will fight the spec. Sorting the codebase into provable vs not-provable before touching the kit is the most actionable takeaway in the piece.