要点
- MSR + GitHub Next + RiSE; Proof-Driven Development toolkit partnered with Chopin planning; Verus verifier for Rust.
- Capstone: ~5,000-line Rust Pet Store (Axum/SQLite + Leptos/Wasm); login request was two sentences, expanded into eight ensures clauses on login_flow.
- Formal vs empirical split made explicit via Trusted Computing Base cards; mutation testing plants one bug per ensures clause to catch "vibe verification."
- Proof covers login_flow and helpers; bcrypt, sqlx, jwt, clock remain trusted-and-tested; CI gains Verus checks and can prune tests already proved.
- Research prototype; Rust/Verus only today; proofs still cost effort; wrong specs verify the wrong thing.
On 5 November 2026, Microsoft Research published a walkthrough of PDD Kit: a research toolkit that tries to make formal methods usable for ordinary full-stack work when coding agents generate more code than humans can read. The setup sits inside Chopin, GitHub Next's shared planning surface. Humans settle intent in plain language. The kit turns formalizable parts into Verus specifications, asks agents to prove the implementation, and writes tests for everything left in the trusted boundary. The thesis is concrete. Once agents emit feature-sized diffs, review must move from line-by-line reading to signed intent that a proof can enforce.
[1]What shipped
PDD Kit is pitched as Spec Kit's cousin for proofs. The workflow has two halves. First, planning questions surface ambiguities a careful reviewer would catch before code exists. Second, approved intent becomes Verus contracts plus empirical checks. Every result is labeled: mathematical proof for all inputs in the formal model, or evidence from tests where the verifier cannot see the code.
The capstone is Pet Store, a ~5,000-line Rust storefront. Backend uses Axum and SQLite; storefront is Leptos compiled to WebAssembly. The blog focuses on login. The developer's request was deliberately rough: only the right password yields a token, and only admin accounts get admin tokens. PDD Kit's decision cards forced the "both ways" reading (token implies right password, and right password always works unless infrastructure fails), which rules out a login that refuses everyone while still "satisfying" a one-sided implication.
The resulting login_flow contract carries eight ensures clauses. Uninterpreted functions model the database and bcrypt so the proof can talk about them without executing them. Trusted wrappers for lookups, password check, token signing, clock, and error mapping each get assumed contracts the developer must accept, plus planned Given/When/Then tests. Mutation checks plant one bug per clause in a scratch copy; if Verus still accepts, the clause constrains nothing.
[1]Evidence on the table
This is a worked research example, not a multi-repo field study. What is hard: a readable intent map tied to Verus snippets; an explicit trusted computing base; CI integration via pdd-ship that fails builds on broken proofs; and a stated habit of pruning tests that only re-check proved properties while keeping tests that guard trusted edges. What is soft: no independent replication, no time-cost table for producing the login proof, and no claim that the whole Pet Store is proved end to end. The authors start where a bug costs most (login, payments, permissions) and grow coverage piece by piece.
They are blunt about vibe verification: models writing their own specs can invent weak invariants that verify while ruling out almost nothing. Reviewer agents and mutation checks are the counterweights. They are also blunt that a wrong spec yields wrong verified code, which is why humans still approve the plain-language plan before prove tasks run.
[1]Steelman and gaps
Steelman. Most production stacks are not Rust, and Verus does not verify TypeScript handlers tomorrow morning. Proof effort remains real; a fuzzy product manager will not enjoy eight ensures clauses. Trusted bcrypt and SQL still carry the password and identity promises. Async completion, timing, and UX judgment stay outside the proof. Teams that rubber-stamp intent cards recreate the old problem one layer up.
Fair. The counter is not that PDD Kit deletes trust. It relocates scarce human attention to the sentences that define correct behavior, then uses a deterministic verifier (Verus + Z3) rather than the same model that wrote the code. For agent-written glue that silently swaps two awaits, that relocation is the whole point.
[1]Who should care, and what to watch
Platform teams adopting coding agents on security-sensitive Rust services should treat intent review as a first-class artifact. Security reviewers gain a receipt that separates proved clauses from trusted ones. Agent-tooling vendors get a target: planning UIs that produce machine-checkable contracts, not only markdown specs. Language communities outside Rust should watch whether the method ports through bindings or new verifiers.
Next six months: public PDD Kit availability and docs quality; more than login modules proved on Pet Store or sibling apps; whether mutation-fail rates stay useful in the wild; and any non-Rust bridge that keeps the same intent-first loop.
[1]Close
PDD Kit's useful sentence is not "formal methods are nice." It is that agent scale breaks exhaustive code reading, so the contract has to become intent a verifier can fail the build on. Six months out, either security-critical agent workflows start merging with proof receipts beside tests, or the kit stays a Microsoft Research demo that busy teams never budget for.
[1]