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