Microsoft Research представила PDD Kit: доказательства для кода от ИИ-агентов

Microsoft Research опубликовала описание PDD Kit: набора инструментов для «разработки, управляемой доказательствами» (Proof-Driven Development, PDD). Исходная проблема, по словам авторов: ИИ-агенты выдают целые функции объёмом в десятки и сотни тысяч строк кода, читать каждую строку pull request уже нельзя, а план, который должен быть «контрактом» между человеком и агентом, ничем не принуждается к исполнению. Агент может реализовать чуть другое, а затем написать тесты, которые проходят для его реализации, а не для задуманного. Покрытие выглядит здоровым, и разрыв между просьбой и результатом всплывает только при баг-репорте или неприятном граничном случае. Тесты проверяют лишь малую часть поведения программы, поэтому нужна другая машинерия, доказательства.

PDD Kit работает как партнёр внутри Chopin, среды совместного планирования в реальном времени от GitHub Next, где команда и агенты работают в одном документе. Процесс состоит из двух половин. Сначала участники в обычном языке уточняют замысел: PDD Kit задаёт вопросы, которые задал бы внимательный ревьюер, объясняет релевантный код и записывает ответы в «артефакт замысла». Те части замысла, что поддаются формализации, превращаются в формальные спецификации на Verus (язык доказательств для Rust). Остальное, что приходится принимать на веру, превращается в неформальные спецификации для тестов. Затем инструмент автоматически генерирует доказательства, что код удовлетворяет формальным спецификациям, и качественные тесты для неформальных. Авторы утверждают, что для этого не нужна подготовка в формальных методах.

Каждый результат помечен видом проверки. Формальная верификация, математическое доказательство, что код отвечает спецификации для любого входа, проверенное верификатором (сегодня это Verus, разработанный совместно Microsoft Research и рядом университетов). Эмпирическая проверка, запуск кода и наблюдение за ним: юнит- и сквозные тесты, автоматизация терминала, браузерные агенты и агенты с управлением компьютером. Она закрывает то, куда доказательство не дотягивается (например, сторонняя криптографическая библиотека или интерфейс). Пройденный тест показывает лишь, что код сработал на опробованных входах, поэтому PDD Kit называет его свидетельством, а не доказательством. Граница между двумя видами, доверенная вычислительная база (TCB): код, о поведении которого доказательство лишь предполагает, что оно такое, как описано. PDD Kit делает эту границу явной и просит разработчика подтвердить каждый элемент.

Демонстрация: Pet Store, полностью написанное на Rust веб-приложение с бэкендом на Axum и SQLite (склад, акции, заказы, оформление покупки) и витриной на Leptos, скомпилированной в WebAssembly; всего около 5 000 строк Rust. Для краткости авторы проверяют только логику входа, но считают, что тот же процесс применим ко всему приложению, и советуют начинать с самых чувствительных частей. Весь запрос разработчика в Chopin уместился в два предложения: проверить логику входа в backend/src/handlers/auth.rs при двух требованиях, «токен выдаётся только при правильном пароле» и «токены администратора получают только учётные записи администраторов».

Шаг 1. Вопросы до кода. Рабочий процесс pdd-plan читает код и до написания чего-либо задаёт вопросы во вкладке Decisions, объясняя контекст так, чтобы ответить можно было, не открывая исходники. Вопрос выглядит педантичным, но важен: требование «токен только при правильном пароле» исключает выдачу токена по неверному паролю, но идеально выполняется и системой, которая отказывает всем. Вторая половина, «правильный пароль всегда работает», обратная импликация; вместе они дают «тогда и только тогда». Оставленный наедине агент выбрал бы одну из половин, не сказав об этом; здесь разработчик выбрал обе.

Шаг 2. Понятная человеку карта замысла. PDD Kit держит вверху плана актуальный раздел: блок-схему логина, «ландшафт спецификации» (что доказывается, чему доверяют) и, где это помогает, мысленную модель; для логина нарисовал «окошко выдачи талонов». Ниже карта замысла связывает каждое требование со словами разработчика и фиксирует, как оно решено, со ссылками на раздел формальной спецификации и покрывающие тесты.

Шаг 3. Доказательство функции логина. Перед сборкой PDD Kit просит утвердить план целиком. Первый черновик доказывал центральное решение логина (выбор таблицы и проверку пароля), а обработчик вокруг оставлял доверенным и тестируемым; это и была рекомендация инструмента. Но разработчик захотел большего: именно в обработчике ожидаются запросы и подписывается токен, и при рефакторинге там легко незаметно поменять две строки местами. Поэтому он на этапе обзора замысла дал обработчику собственную асинхронную спецификацию, чтобы доказательство покрывало и эту «склейку». Новая асинхронная функция login_flow несёт контракт от полей запроса до токена или HTTP-ошибки. Пересмотренный план PDD Kit вынес на повторное утверждение: соответствие замыслу, не доказательство и не одобряет новое доверие или более широкий охват.

Шаг 4. Где доказательство кончается. Для логина не доказуемо многое: код, которого верификатор не видит (bcrypt, sqlx, jsonwebtoken лежат в других крейтах); факты внешнего мира (что сейчас в SQLite и сколько на часах); завершится ли работа и как быстро (зависший или медленный запрос ничего в спецификации не нарушает); то, что оценивает человек (понятно ли сообщение об ошибке); и то, что никто не записал. Эти места закрывает эмпирическая проверка: PDD Kit оборачивает каждый доверенный элемент в небольшую функцию с принятым контрактом (через #[verifier::external_body] или external_fn_specification), просит принять каждый отдельно и вписывает в план тест на каждое допущение. Для логина разработчик подтвердил шесть элементов: два поиска (Customer::find_by_email и Admin::find_by_username возвращают ровно строку своей таблицы или ничего); check_password, тонкая обёртка над bcrypt::verify (ошибка только на нечитаемом хеше, Ok(true) означает ровно правильный пароль); generate_token (подписывает ровно переданные утверждения секретом из конфигурации, сбой подписи отдаёт как 500); expiry_from_now (читает часы и записывает срок ровно на 24 часа позже); database_error (превращает сбой поиска в нынешнюю ошибку 500 с сообщением sqlx); и оболочка обработчика входа. Текст источника обрывается на описании последнего элемента.

Итог, как его формулируют авторы: Verus усилил код и выявил уже имевшиеся ошибки, доказав отсутствие ошибок входа относительно спецификации, а разработчик проверял замысел и ни разу не читал сгенерированный код построчно.

Ключевые факты

• PDD Kit, набор инструментов Microsoft Research для Proof-Driven Development: превращает замысел разработчика в формальную спецификацию на Verus, доказывает код агента и подключает тесты там, где доказательство не достаёт.
• Работает внутри Chopin от GitHub Next; каждый результат помечен как формальное доказательство или эмпирическая проверка (тесты, лишь «свидетельство»), а доверенные допущения разработчик подтверждает по одному.
• Демо на приложении Pet Store (около 5 000 строк Rust): проверяли только логику входа по запросу из двух предложений; разработчик выбрал более строгий вариант, доказав и обработчик через асинхронную функцию login_flow.
• По словам авторов, Verus выявил уже имевшиеся ошибки и доказал отсутствие ошибок входа относительно спецификации; разработчик не читал код построчно.
• Доказательство не покрывает внешние библиотеки, состояние внешнего мира, время и завершение работы, оценку человеком и всё, что не записано в спецификации.

Почему это важно

Агенты пишут функции объёмом в десятки и сотни тысяч строк, и построчное чтение кода, по оценке авторов, перестаёт масштабироваться. Тесты, которые агент пишет сам, обычно проверяют то, что он построил, а не то, что у него просили. PDD Kit предлагает другой рычаг контроля: ревьюер проверяет замысел и границы доверия, а соответствие кода замыслу подтверждает верификатор. Авторы позиционируют это как перенос формальных методов от узких специалистов к обычным инженерам и рядовым приложениям, таким как полноценное веб-приложение.

Кому это важно

Командам, где код во многом пишут ИИ-агенты и где ошибка в чувствительной части (вход, права доступа, платежи) стоит дорого. Разработчикам на Rust, которые уже используют или присматриваются к Verus. Тем, кто отвечает за ревью и качество, и кому надоело, что покрытие тестами выглядит хорошо, а разрыв с исходным замыслом скрыт.

Как это применить

Авторы советуют начинать с самых чувствительных частей приложения и верифицировать его постепенно; в демо взят вход в систему. Рабочий порядок: описать требования грубо (в демо хватило двух предложений), ответить на вопросы PDD Kit до появления кода, утвердить план и список доверенных элементов, затем пересмотренный план. Сегодня верификатором служит Verus для Rust, а среда запуска, Chopin от GitHub Next. Сведений о выпуске, доступности и лицензии PDD Kit в доступной части текста нет.

Можно ли доверять

Источник, блог Microsoft Research, то есть описание собственного инструмента его авторами; независимых оценок и сравнения с другими агентами или средствами верификации в тексте нет. Демонстрация охватывает один пример и только логику входа. Число и характер найденных ошибок в доступной части не названы, как и размер доказательства, время проверки или затраты труда. Текст источника обрывается на списке доверенных элементов, поэтому итоговый раздел виден лишь частично.

Риски и подводные камни

Доказательство покрывает только свою спецификацию и ничего не говорит о требованиях вне её. Оно не охватывает код, которого верификатор не видит (bcrypt, sqlx, jsonwebtoken), состояние внешнего мира (содержимое SQLite, показания часов), завершение и скорость работы, а также то, что должен оценивать человек. Всё это остаётся на доверенных допущениях и тестах, а пройденный тест, лишь свидетельство на опробованных входах. Если допущение в TCB неверно, доказательство опирается на ложную посылку; поэтому каждый доверенный элемент нужно осознанно принимать. Кроме того, обработчик в демо доказывали по решению разработчика сверх рекомендации инструмента, то есть глубина охвата зависит от принятых на обзоре решений.

«Токен выдаётся только при правильном пароле.»

— разработчик (имя не названо), первое из двух требований в запросе в Chopin