Code review does not scale to how much code agents can write in a day, and a test suite only proves the specific cases somebody remembered to write. Microsoft Research and GitHub Next shipped something this week that closes that gap with proof instead of sampling. Proof-Driven Development Kit takes a plan written in Chopin, GitHub Next's planning prototype, and translates it into Verus contracts in Rust: preconditions, postconditions, invariants. An agent writes the implementation and the verification annotations side by side. Verus generates proof obligations from that and hands them to an SMT solver. Code ships only once every required obligation is discharged, not once it happens to pass whatever tests existed. This builds directly on GitHub's own Spec Kit, which has spent the last year pushing spec-driven development as mostly a prompting discipline, written requirements steering what Copilot does. PDD Kit's actual contribution is enforcement. The spec stops being guidance a model can quietly ignore and becomes something a theorem prover checks mechanically, every time. It's not a universal fix and the team is upfront about that. The method only verifies what the specification states, and an LLM can still write a spec that drops a requirement or misreads the plan entirely. Unsafe Rust, foreign interfaces, and anything outside the formal model sit outside the proof. Architecture and security boundaries still need a person looking at them. Formal verification has lived in a small, expensive corner of software for decades, aerospace, crypto, medical devices, places where a bug was unacceptable rather than merely annoying. Agents writing most of the code may be what finally drags it into everyone else's stack.