You Review the Spec, the Machine Reviews the Code

GitHub Next and Microsoft Research announced the Proof-Driven Development Kit on October 21. It is in research preview, it only works on Rust, and it makes an argument that most teams running coding agents have been avoiding: if you can't read the diff line by line anymore, stop pretending you can, and review something else instead.

The something else is a specification. In the kit's workflow, a human approves the spec, and a machine checks the implementation against it for every possible input.

Five steps, and where the human sits

The loop runs like this. A team plans the feature inside Chopin, GitHub Next's multiplayer agentic planning tool. The kit then discusses the code, infers intent, and proposes a formal specification written in Verus, an existing open-source proof language for Rust. A human approves the spec — not the code. Verus then proves the agent's generated code satisfies that spec for every input. Where a full proof isn't possible, the kit falls back to tests and computer-use agents for empirical checking, and the output is a verified pull request.

The inversion is the whole idea. You review the requirement. The verifier reviews the implementation. In Verus, a spec annotates functions with preconditions and postconditions the verifier must discharge, and the guarantee is stronger than a green test suite in a specific way: tests sample inputs, proofs quantify over all of them.

GitHub's own framing is that Chopin plus the kit lets teams ship AI-generated code to production without reviewing it line by line, with stronger assurance than code review and testing alone. That's a vendor describing its own research preview, not an audited result. Hold it loosely.

The cost moved, it didn't disappear

There's a temptation to read this as "the review burden is solved." It isn't. It moved to the front of the pipeline, and it got harder in a way that's easy to underestimate.

Writing a spec precise enough to be provable is a different skill from reviewing a diff. Vague requirements produce unprovable specs, and the verifier will tell you so by failing, which means the first few weeks of adoption look like a tool that doesn't work. What's actually happening is that the ambiguity in your requirements is being surfaced earlier than usual, by something that won't paper over it with a plausible-looking function.

For teams that already write design docs nobody reads, this is a real change. The design doc becomes load-bearing, because it's the artifact that gets checked.

Where the proofs stop

Three limits matter more than the feature list.

Rust only. Verus checks Rust, and GitHub Next says the kit works on Rust today, with no new language and no change to how the code is produced. If your agents write TypeScript or Python, there is nothing to install yet. Given how much production code is not Rust, this is a large restriction wearing a small sentence.

Only what a spec can express. Formal proof covers properties you can state precisely: input and output contracts, invariants, state machine transitions. It does not cover UI behaviour, most I/O-heavy logic, or anything where "correct" is a judgment rather than a property. All of that goes down the fallback path of tests and human review, which is exactly where today's burden already lives.

Research preview, with a specific history. Chopin is listed on GitHub Next's projects page as a research prototype dated September 2026. GitHub Next has shipped prototypes before — Repo Mind, Project Copernicus, SpecLang among them — that never reached general availability. The first public demo against real code is scheduled for GitHub Universe, October 28–29.

The fallback is where the honesty lives

The design decision that says the most isn't the prover at all. It's the explicit second path for code that can't be proved, which routes to tests and computer-use agents for empirical checking.

That's an admission most verification tools refuse to make. It says, in the architecture, that some code is provable and some isn't, and that pretending otherwise would be worse than shipping two pipelines. A team using this ends up with a per-module label — proved, tested, reviewed — which is a more honest inventory of confidence than anything a coverage report produces.

The catch is that the fallback path is also where agents grade their own homework. A computer-use agent clicking through a UI to check whether a change worked is still an agent, still sampling, and still capable of concluding that a broken flow looks fine. The proved path is a proof. The fallback is a demo that passed.

The research underneath is the reassuring part

The kit isn't a verifier built from scratch. Verus is separate and established. Microsoft Research's verus-proof-synthesis repository holds the groundwork: two LLM-driven systems, AutoVerus and VeruSAGE, that generate and repair Verus proofs, benchmarked against 150 and 849 verification tasks respectively.

What the kit appears to add is packaging. This is the first time that line of proof-synthesis research has been folded into a plan-to-PR product workflow rather than a benchmark exercise. That's a smaller claim than "AI can prove its own code," and a more credible one.

Note also that sources can't agree on the name. You'll see Proof-Driven Development Kit and Property-Driven Development Kit in the same week's coverage, both attributed to the same announcement. Pick one and move on; the acronym is doing the branding either way.

What you can do today

The durable takeaway isn't "wait for GA." It's that an agent-heavy codebase now splits into provable and non-provable territory, and your configuration should already know which is which.

Parsers, state machines, data structure invariants, arithmetic with bounds, concurrency primitives — that's provable territory, and Verus is open source and usable now, with or without the kit. Most front-end work, most glue code, and anything whose correctness depends on what a user meant is not.

Two practical moves follow. First, tag the provable modules in your repo and point your agents at Verus for those specifically, before any vendor ships a workflow. Second, stop asking agents to also write the tests that validate their own work; that arrangement has always been a conflict of interest, and it's the reason a green suite means less than it used to.

The uncomfortable question

If a spec can be approved by a human and a proof discharged by a machine, what exactly is the reviewer for? Not for reading code, and probably not for catching the bug the agent introduced on line 412.

The reviewer's job becomes the one it should have been all along: deciding what the system is supposed to do, and refusing to accept a specification that doesn't say it. That's harder than clicking approve on a diff. It's also the only part of the work that a verifier can't do for you.