GitHub Next представила PDD Kit для доказательной проверки кода ИИ-агентов на Rust

GitHub Next и Microsoft Research выпустили в исследовательском превью Proof-Driven Development Kit: человек утверждает формальную спецификацию на языке Verus, а верификатор доказывает соответствие ей сгенерированного агентом кода для всех входных данных. Инструмент работает только с Rust, а там, где полное доказательство невозможно, откатывается к тестам.

• Работает только с Rust: спецификации пишутся на открытом языке доказательств Verus
• Человек проверяет спецификацию, а не каждую строку диффа от агента
• Опирается на исследования AutoVerus и VeruSAGE, проверенные на 150 и 849 задачах
• Публичная демонстрация на реальном коде — на GitHub Universe 28–29 октября 2026 года