Как формально проверять веб-приложения, созданные ИИ-агентами, с помощью PDD Kit

Зачем проверять план

Агенты для программирования уже создают целые функции за один сеанс — иногда десятки и сотни тысяч строк. Построчная проверка таких изменений плохо масштабируется, поэтому команды чаще согласуют с агентом план и тесты, а затем передают ему реализацию.

Но план на естественном языке сам по себе не заставляет агента ему следовать. Агент может реализовать немного другое, а затем написать тесты, которые проверяют именно получившийся код. В результате проверок и строк покрытия становится больше, но расхождение между запросом и программой может обнаружиться только после сообщения об ошибке или редкого случая.

Тесты проверяют лишь часть возможных входных данных. Формальное доказательство может показать, что код выполняет заданные требования для каждого входа, охваченного спецификацией. Раньше такой подход требовал специалистов, отдельных языков и долгой работы. По словам авторов, теперь ИИ-агенты всё лучше помогают составлять формальные спецификации и доказательства. Для этого процесса они используют термин Proof-Driven Development (PDD) и создали PDD Kit.

Работу представили в контексте Microsoft at SOSP 2026 — площадки, где академические и промышленные участники обсуждают теорию и практику системного программного обеспечения.

Как работает PDD Kit

PDD Kit — набор инструментов для формальных методов, устроенный примерно так же, как Spec Kit для разработки по спецификации. Он работает внутри Chopin — среды GitHub Next для совместного планирования в реальном времени, где команда и агенты редактируют общий документ.

Сначала участники команды уточняют намерения обычным языком. PDD Kit задаёт вопросы, объясняет связанные с ними части кода и записывает ответы в документ намерений. Он связывает исходные требования с формальной спецификацией и тестами. То, что можно выразить формально, становится спецификацией; остальное оформляется как неформальные требования для тестирования. Затем система готовит доказательства для формальной части и тесты для остальной. Для работы с PDD Kit не требуется опыт в формальных методах.

Каждый результат отмечает, каким способом его проверили:

Граница между проверенным и принятым на доверии кодом называется доверенной вычислительной базой (TCB). PDD Kit обозначает её явно и просит разработчика отдельно подтвердить каждую часть.

Приложение Pet Store

Чтобы проверить подход на существующей кодовой базе, команда создала Pet Store — веб-приложение, полностью написанное на Rust. Серверная часть использует Axum и SQLite, работает с запасами товаров, скидками, заказами и оформлением покупок. Интерфейс создан на Leptos и компилируется в WebAssembly. В приложении около 5 000 строк Rust.

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

В Chopin разработчик сформулировал требования двумя пунктами:

Запрос намеренно оставили кратким: задача PDD Kit — уточнить намерение и превратить его в требования, которые можно проверить доказательством.

Разработка на основе доказательств с PDD Kit. Члены команды согласовывают намерение. Verus и набор тестов следят, чтобы код ему соответствовал

Источник: microsoft.com

От уточнений к карте требований

Перед написанием кода этап планирования pdd-plan изучает проект и показывает вопросы во вкладке решений. Если вопрос зависит от устройства программы, система сначала объясняет соответствующий фрагмент: его назначение, связи с другими частями и конкретную функцию.

Одно из уточнений касалось формулировки «токен выдаётся только при правильном пароле». Она запрещает выдать токен при неверном пароле, но сама по себе не требует выдавать его при верном: программа, которая отказывает всем, тоже выполняет это условие. Чтобы исключить такой вариант, нужно добавить обратное требование — правильный пароль всегда даёт токен. Первое условие означает «если выдан токен, пароль правильный», второе — «если пароль правильный, выдаётся токен». Вместе они образуют условие «тогда и только тогда». Без уточнения агент мог бы выбрать одну трактовку молча; разработчик подтвердил обе.

По мере обсуждения PDD Kit поддерживает краткое описание работы в начале плана, чтобы команде не приходилось искать решения в длинной переписке. В нём есть схема входа, обзор того, что будет доказано или принято на доверии, и, если нужно, наглядная модель. Для входа система нарисовала стойку выдачи билетов.

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

Первая карточка решения. Условие «только с правильным паролем» само по себе выполняет и система входа, которая никого не пускает. Проверка в обе стороны исключает такой вариант

Источник: microsoft.com

Как проверяли вход

Перед началом работы команда должна подтвердить план целиком. В первом варианте PDD Kit предложил доказать основную логику входа — выбор таблицы и проверку пароля, — а окружающий обработчик оставить доверенным и покрыть тестами. Разработчик решил включить в доказательство и обработчик: именно там ожидаются результаты запросов к базе данных и подписывается токен, поэтому при изменении кода можно случайно переставить строки.

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

Что доказывается, а чему доверяют при входе. Зелёные функции Verus доказывает для любого ввода. Янтарные элементы считаются доверенными, принимаются разработчиком и проверяются запланированными тестами из §4.1 плана

Источник: microsoft.com

Карточка доверия для check_password. Verus принимает эти два условия на веру, поэтому человек принимает их, а два теста проверяют

Источник: microsoft.com

Запланированный тест для доверенного check_password, написанный до появления самого теста. В плане успешный тест обозначен как свидетельство, а не доказательство

Источник: microsoft.com

Модель входа в PDD Kit. Переданное поле выбирает окно, окно выбирает таблицу, а вместе с ней — роль; ничего не выводится, пока пароль не совпадает

Источник: microsoft.com

Что осталось за границей доказательства

Доказать можно не всё. В проверке входа PDD Kit выделил несколько ограничений:

Для таких частей используется эмпирическая проверка. PDD Kit обозначает границу доверия и оборачивает каждый непроверяемый компонент небольшой функцией с контрактом-предположением. В Verus для этого применяются #[verifier::external_body] или external_fn_specification. Разработчик принимает каждый контракт отдельно, а план получает тест на каждое его условие.

В примере команда подтвердила шесть частей:

Для поиска по базе данных код остаётся на прежнем месте, а внешний контракт описывает, что он должен вернуть. В примере контракт ex_customer_find_by_email задаёт условие: успешный запрос возвращает запись клиента, соответствующую точному адресу электронной почты, или None, если записи нет. Сам запрос выполняется в sqlx и недоступен для проверки Verus.

Часы вынесены в обёртку expiry_from_now, помеченную #[verifier::external_body]. Verus использует её условие и не проверяет тело функции: срок действия должен наступить ровно через 86 400 секунд после чтения часов. Функция по-прежнему может аварийно завершиться, если время выходит за допустимые пределы; гарантия от этого не даётся.

Запись в карте намерений после принятия решения: при входе токен выдаётся только при правильном пароле для этой учётной записи и всегда выдаётся при нём. Блок-схема показывает все возможные исходы проверки пароля

Источник: microsoft.com

PDD Kit показывает, что именно доказывает Verus, что люди принимают и проверяют тестами, а также что остаётся без обещаний. Каждый выбор границы доверия вынесен в отдельную карточку: в ней указаны принятые условия и последствия, если предположение окажется неверным. Для каждого такого условия план предусматривает эмпирическую проверку в формате «Дано / Когда / Тогда». До запуска она отмечена как запланированная; после запуска сохраняются результат команды и коммит, на котором её выполнили.

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

Два прочтения одного и того же предложения. Они различаются одной ячейкой, и от этой ячейки зависит, что должно установить доказательство

Источник: microsoft.com

Спецификация и код входа

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

Для требования о пароле важно, что проверка пароля и выданный токен относятся к одному аккаунту. Например, ошибка могла бы позволить проверить пароль Боба, а токен выпустить для аккаунта Алисы. Отдельные шаги выглядели бы правильными, но формальное условие выявило бы несоответствие.

Спецификация описывает SQLite, bcrypt и JWT без запуска этих компонентов. Для этого используются абстрактные функции без тела: customer_on_file(email) и admin_on_file(username) обозначают записи в базе, bcrypt_verdict(password, hash) — результат проверки bcrypt, а token_claims(token, secret) — содержимое токена. Verus знает об их поведении только то, что обещают доверенные контракты.

Определение named_account(email, username) указывает, какой аккаунт соответствует запросу: сначала запись покупателя для указанного адреса; если адрес не передан — запись администратора для имени пользователя; в остальных случаях аккаунта нет. Это похожий на Rust математический код, который не запускается и существует только в контрактах. Такой код называют призрачным: проверяющая система учитывает его, а компилятор удаляет из программы.

Два исходных требования разработчика превратились в восемь условий для login_flow. Они описывают, в частности, следующие случаи:

Контракт check_password связывает функцию с абстрактным результатом bcrypt: ответ успешен тогда, когда bcrypt может прочитать хеш; значение ответа определяет, правильный ли пароль. Тело функции Verus не проверяет, поэтому все обещания о пароле в login_flow зависят от этого принятого контракта. Доказательство охватывает все варианты результата входа, но только один из них содержит токен.

Функция login_flow асинхронная и ожидает запрос к базе данных. Verus позволяет задавать контракты для асинхронных функций: requires проверяется при создании задачи, а ensures — для результата после её ожидания. Гарантии того, что задача завершится, нет; зависший запрос не нарушает условия.

Логика разделена на небольшие функции. lookup_target выбирает таблицу, login_core ожидает результат поиска и передаёт управление функции decide_login, которая проверяет пароль. issue_token подписывает токен или преобразует отказ в существующую HTTP-ошибку. У каждой функции свой контракт, и Verus использует эти контракты, доказывая поведение login_flow. Если изменить тело decide_login, повторно доказывать нужно только эту функцию.

Контракт lookup_target задаёт выбор таблицы: переданный адрес электронной почты направляет поиск к покупателям; если адреса нет, имя пользователя направляет поиск к администраторам; если нет ни того ни другого, вход отклоняется из-за отсутствия идентификатора. decide_login отказывает, если запись не найдена, выдаёт утверждения только при совпадении пароля и назначает роль в зависимости от таблицы, в которой нашлась запись.

Чтобы доказать больше свойств входа, нужно доверять большему числу небольших обёрток. На карточке это указано до того, как разработчик сделает выбор

Источник: microsoft.com

Файл спецификации verified/src/login.rs устроен в четыре слоя: необходимые Verus типы и импорты, абстрактная модель внешнего мира, контракты доверенных частей и пять контрактов, которые должно выполнить доказательство. В частности, пул соединений остаётся непрозрачным для проверки, а поля записи клиента доступны.

Отдельный тип LoginError отделяет причину отказа от HTTP-ответа. Благодаря этому issue_token связывает каждый отказ с существующим статусом: отсутствие адреса и имени пользователя — 400, отсутствие аккаунта или неправильный пароль — 401, ошибка чтения хеша или запроса к базе данных — 500.

До возвращения плана два агента-рецензента ищут ошибки в формальной спецификации, созданной по документу намерений. Они проверяют, соответствует ли она запросу и не обещает ли больше, чем можно доказать. Уточнение спецификации выполняется в фоне и учитывает ответы пользователя, пока рецензенты не согласятся, что она корректна.

Доказательство, тесты и проверка требований

После подтверждения спецификации разработчик больше не проверяет реализацию построчно: её и доказательство проверяют машины. Этап сборки передаёт план pdd-prove, который превращает его в список задач. Для логики входа было семь задач: подготовить login.rs к сборке с Verus внутри серверной части, доказать решения, выдачу токена и полный путь входа, а затем создать тесты для доверенных обёрток и сценария целиком.

Каждая задача проходит одинаковый цикл:

Проверяется и сама спецификация. Когда модель пишет собственную спецификацию или её настраивают на создание доказательств, она может выбрать слабые инварианты: формально проверяемые условия, которые почти ничего не ограничивают. Авторы называют такую проверку «проверкой на ощущениях». Чтобы обнаружить слабые условия, pdd-prove меняет код: для каждого условия ensures в отдельной копии добавляет ошибку — например, отказывает всем или ищет имя пользователя раньше электронной почты. Verus должен отвергнуть каждую ошибочную версию именно по соответствующему условию. Если ошибка проходит, условие не ограничивает поведение и считается пробелом.

Процесс не позволяет незаметно менять требования. Если конструкцию нельзя выразить в закреплённой версии Verus, задача останавливается и возвращается команде — система не заменяет асинхронную функцию синхронной и не ослабляет контракт.

Где заканчивается доказательство для входа. Verus доказывает корректность ядра для любого ввода. Люди принимают доверенное кольцо, а тесты его проверяют. В плане перечислено то, что никто не обещает

Источник: microsoft.com

Проверка кода и дальнейшая работа

После прохождения задач pdd-prove открывает запросы на включение изменений. Они добавляют отдельный пакет verified/ с login_flow, вспомогательными функциями, доказательствами и доверенными обёртками с тестами. Настоящий обработчик направляет запросы через login_flow, сохраняя существующие HTTP-статусы. Проверенная логика подключается к рабочему пути входа, а не к отдельной копии приложения.

Разработчик смог включить изменения, не проверяя весь сгенерированный код построчно. Основная проверка требований уже прошла при работе с документом намерений, где последнее слово остаётся за командой. Запрос на включение изменений показывает, какие требования доказаны формально, а какие проверены тестами.

При слиянии PDD Kit добавляет проверку Verus в CI рядом с тестами. Последующие изменения входа — от человека или агента — должны по-прежнему соответствовать той же спецификации; нарушенное доказательство останавливает сборку, как и проваленный тест. Кроме того, система удаляет тесты, которые повторяют уже доказанные свойства, например отдельные примеры для проверки пароля, и сохраняет тесты доверенной границы.

Авторы разделяют гарантии на три группы:

Почему Rust

Сейчас PDD Kit проверяет только Rust — на нём работает Verus. Если проект уже написан на Rust, перенос не требуется. Код на других языках можно перенести на Rust и проверить по той же спецификации; проекты не на Rust могут вызывать проверенный код Rust через связующие интерфейсы.

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

Ограничения и дальнейшие планы

PDD Kit — исследовательский прототип, который пока поддерживает только Rust. Доказательства требуют реальной работы, главным образом на их подготовку. Ясная спецификация снижает эти затраты, поэтому значительная часть инструментария посвящена уточнению намерений. Авторы рекомендуют начинать с мест, где ошибка обходится дороже всего, например с входа, платежей или прав доступа, а затем проверять остальные части проекта по одной.

В Pet Store формально проверили один фрагмент одного приложения: читаемую спецификацию, доказательство Verus и тесты для того, что принято на доверии. Гарантии зависят от шести таких частей; больше всего — от check_password, на котором держатся обещания о паролях, и двух запросов к базе данных, от которых зависит правильность выбранного аккаунта. Тесты поддерживают эти предположения, но не доказывают их. Авторы ожидают, что со временем доверенная граница заметно сократится, и хотят проверить, насколько далеко можно масштабировать подход.

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

Благодарности

Работу выполнили Microsoft Research Catalyst Lab, GitHub Next и группа Research in Software Engineering (RiSE). Авторы поблагодарили Мэгги Эпплтон и Кшиштофа Цесляка из GitHub Next за совместную работу над Chopin, а также Никхила Свами, Лефа Иоаннидиса, Джанардхана Кулкарни и Шувенду Лахири — за отзывы и обсуждения формальной проверки и формализации намерений. Команды F*/Pulse и Verus помогали проекту; Идан Газит из GitHub Next поддерживал сотрудничество.

Ответы на частые вопросы

Если спецификацию пишет ИИ, кто проверяет, что она верна?

Разработчик: доказательство показывает, что программа соответствует спецификации, но не подтверждает, что спецификация передаёт задуманное. Поэтому pdd-plan изучает код, задаёт вопросы до написания спецификации и превращает ответы в план на обычном языке и спецификацию Verus для согласования. Два агента-рецензента дополнительно проверяют спецификацию, а pdd-prove добавляет по одной ошибке на каждое условие, чтобы находить условия, которые ничего не ограничивают. Ошибочная спецификация всё равно возможна, поэтому разработчику нужно явно записать требования, разобрать неоднозначности и подтвердить план до начала проверки.

Чем PDD отличается от разработки по спецификации, разработки через тестирование и самопроверки агента?

Различие — в том, что удерживает код в рамках плана. При разработке по спецификации её соблюдение ничем не обеспечивается. Разработка через тестирование проверяет образцы входных данных, причём тесты нередко пишутся под уже созданную реализацию. При самопроверке работу оценивает та же модель, которая написала код. В PDD Verus автоматически проверяет доказательство соответствия одобренной спецификации. Подход сохраняет планирование, знакомое по разработке по спецификации, и добавляет тесты там, куда доказательство не распространяется. Тест проверяет некоторые входы; доказательство подтверждает заданные свойства для всех входов формальной модели с учётом её предположений.

Что именно доказывается и где запускается проверка?

Доказательство — это код Rust с конструкциями Verus. Verus механически проверяет его с помощью решателя Z3. Проверка работает там же, где собирается Rust: pdd-prove запускает её во время подготовки доказательства, а pdd-ship добавляет её в сборку и CI. Проверка детерминированная, модели в ней не участвуют: модели могут писать спецификацию, код и доказательство, но результат определяет запуск Verus. Для небольшого модуля он обычно занимает секунды, для крупной кодовой базы — до нескольких минут; время зависит от размера кода и сложности доказательств.

Что проверяет разработчик, если построчная проверка заменяется?

PDD Kit переносит основное внимание на требования к поведению программы. Разработчик проверяет план на обычном языке, формальную спецификацию и доверенные компоненты за пределами доказательства. Запрос на включение изменений перечисляет, что формально доказано, что проверено тестами и где может понадобиться дополнительная проверка. В Pet Store такой подход сократил зависимость от исчерпывающего просмотра сгенерированного кода построчно.

Поддерживаются ли другие языки и почему выбрали Verus?

Сейчас проверяется только Rust. Verus позволяет проверять код Rust напрямую, что соответствует задаче PDD Kit — встроить формальную проверку в существующий процесс разработки на Rust. Другие языки доказательств, включая Lean, F* и Rocq, используют другие подходы и имеют свои особенности. Методы PDD Kit, по мнению авторов, могут помочь применять и их.

Авторы проекта — Алекс Лаваи и Маттай Филипозе.

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