# Microsoft Research explains Proof-Driven Development for trusting AI-generated code

> Original title: How do you solve the trust problem with AI-generated code?

- Source: Microsoft Research
- Published: 2026-11-05T18:36:02.000Z
- Bad Influence: https://badinfluence.news/items/amproch5zjbf7iavpowgc4s6c
- Original: https://x.com/MSFTResearch/status/2118412037793480829

## Summary

Microsoft Research describes Proof-Driven Development Kit, which turns plain-language developer intent into a specification in Verus and applies formal methods to check AI agent-generated code. PDD Kit uses mathematical proofs to test code against the spec where possible and indicates where the proofs cannot reach.

## Post

How do you solve the trust problem with AI-generated code?

AI agents can generate code at a scale too great for humans to review line-by-line. That makes it difficult to ensure the code will do what the developer intended, and it leaves the final output vulnerable to bugs and security risks. 

Proof-Driven Development Kit turns plain-language developer intent into a specification in Verus, applying formal methods traditionally used for safety-critical systems. PDD Kit uses mathematical proofs to test agent-generated code against the spec where possible, and clearly indicates where the proofs can’t reach. The result is more reliable agentic code. 

Researchers @MatthaiP39719  and @alexlavaee break down Proof-Driven Development in the MSR blog: https://msft.it/6019af2V7

[Video](https://badinfluence.news/api/img-proxy?u=https%3A%2F%2Fpbs.twimg.com%2Fmedia%2FHWYceG0XQAAwSHL.png&mode=thumb&exp=1794096000&sig=cd24bde68f990320)