# Microsoft's PDD Kit Makes Formal Math Proofs a Gate for AI Rust Code

AlphaSignal, 2026-10-21. [Read the original](https://alphasignal.ai/news/microsoft-s-pdd-kit-makes-formal-math-proofs-a-gate-for-ai-rust-code).

Microsoft Research released PDD Kit, which uses Verus to make a formal proof a gate that AI-written Rust code must pass.