Microsoft Research представляет PDD Kit для формальной верификации кода, написанного ИИ
PDD Kit переводит намерения разработчика в формальные спецификации, доказывая, что сгенерированный агентами код работает корректно для любых входных данных.
Главное за 30 секунд
PDD Kit позволяет разработчикам проверять правильность сгенерированного ИИ кода с помощью математических доказательств, устраняя необходимость построчного ревью больших объемов кода.
- Инструмент использует язык Verus для создания формальных спецификаций кода на Rust.
- PDD Kit был успешно протестирован на веб-приложении Pet Store объемом около 5000 строк кода.
- Система четко разделяет формально доказуемый код и код, требующий эмпирического тестирования (TCB).
Неочевидное: Развитие самих ИИ-агентов сделало возможным применение ранее слишком дорогих и сложных формальных методов верификации в повседневной разработке.
Суть
Microsoft Research представила PDD Kit — набор инструментов для нового подхода к разработке, названного Proof-Driven Development (разработка на основе доказательств). Этот инструмент решает растущую проблему масштабирования проверки кода, сгенерированного ИИ-агентами. Вместо того чтобы построчно вычитывать тысячи строк, разработчик формализует свои намерения, а система математически доказывает, что код агента им соответствует.
Контекст
Современные ИИ-агенты для написания кода способны создавать целые функции за один присест, генерируя десятки и сотни тысяч строк. Традиционный процесс проверки (code review), при котором человек читает каждую строку, перестает масштабироваться.
Обычно разработчики составляют план (контракт) на естественном языке и передают его агенту вместе с тестами. Однако на практике агент может отклониться от плана, реализовать что-то немного иное и написать тесты, которые проходят именно для его реализации, а не для изначальной задумки. Это приводит к разрастанию баз тестов и скрытым ошибкам, которые обнаруживаются только в крайних случаях.
Flow diagram showing the PDD Kit workflow for formally verifying agent-written code. Team members review intent by expressing requirements in plain language, which are formalized in a pdd-plan containing decision cards, intent artifacts, trusted boundaries, and reviewer approvals. The plan generates a formal specification with Verus ensures clauses. Machines then check the code through pdd-prove, which includes Verus proofs, tests for trusted components, and LLM gap review. Verified code and receipts are submitted as a pull request. Dashed feedback loops return specification contradictions and verification gaps to earlier planning and coding stages.
Детали
PDD Kit работает как партнер внутри Chopin, многопользовательской среды планирования от GitHub Next. Процесс состоит из двух этапов:
- Согласование намерений (Questions before code): PDD Kit анализирует код и задает уточняющие вопросы разработчику на простом языке. Ответы фиксируются в «карте намерений» (intent artifact).
- Генерация доказательств и тестов: Инструмент переводит формализуемую часть намерений в спецификации на языке Verus (язык доказательств для Rust). Затем он автоматически генерирует математические доказательства того, что код удовлетворяет спецификациям для любых входных данных. Для частей, которые невозможно доказать формально (например, UI или сторонние криптографические библиотеки), создаются надежные тесты (эмпирическая верификация).
Граница между формальным доказательством и тестами называется доверенной вычислительной базой (Trusted Computing Base, TCB). Разработчик должен явно подтвердить каждую часть TCB.
Команда Microsoft Research успешно применила PDD Kit на Pet Store — полностековом веб-приложении на Rust (около 5000 строк кода), использующем Axum, SQLite и WebAssembly (Leptos). В частности, была формально верифицирована логика авторизации, что позволило выявить существующие ошибки и доказать отсутствие багов входа в систему относительно спецификации, при этом разработчик не читал сгенерированный код построчно.
Также по темеИИ-агенты в химии: как платформа Antigravity ускоряет разработку лекарств
Screenshot of a verification tool evaluating a login authentication requirement. The prompt asks, “Must the right password always get a token?” A flow diagram shows a login request leading to a password check, where matching passwords receive a token and non-matching passwords are refused. Option A, highlighted as recommended, proves both outcomes: the correct password receives a token and an incorrect password is refused. Option B proves only that incorrect passwords are refused, leaving the result for the correct password unspecified.
Анализ
Переход от тестирования к формальным доказательствам (Proof-Driven Development) означает качественный сдвиг в обеспечении надежности ПО. Математическое доказательство отвечает на вопрос «Верно ли это?», в то время как ревью — только «Выглядит ли это верным?».
Ранее формальные методы считались слишком дорогими и требовали узких специалистов, экзотических языков и долгих лет разработки. Однако развитие ИИ-агентов изменило ситуацию: они теперь могут помогать как в написании формальных спецификаций, так и в генерации самих доказательств. Это делает строгие математические проверки доступными для повседневной разработки без необходимости глубоких знаний в области формальных методов.
Перспектива
Подход PDD Kit может стать стандартом для работы с ИИ-агентами, особенно в критически важных частях приложений, таких как аутентификация или финансовые транзакции. По мере того как ИИ будет писать все больше кода, роль человека окончательно сместится от написания и проверки строк кода к четкому формулированию намерений и управлению контрактами.
Three-panel illustration comparing login outcomes. In the first panel, a customer logs in with the correct email and password and receives a “customer” ticket. In the second panel, the same email is paired with an incorrect password and access is refused. In the third panel, an administrator logs in with the correct username and password and receives an “admin” ticket. The diagram uses a ticket-counter analogy to explain authentication and role-based access.
Comparison of two approaches to verifying a login handler. Option A, recommended, keeps the login handler trusted and verifies only the login decision logic, while database lookups and token signing remain tested but trusted components. Option B gives the login handler its own formal specification, proving the orchestration logic but requiring additional trusted wrappers and assumed contracts around database lookups, clocks, and JWT signing.
Diagram showing the proof boundary for a formally verified login system. Functionality outside the proof is either not promised or trusted and validated through human review and testing, including SQLite lookups, bcrypt, the system clock, JWT signing, database error handling, and request parsing. At the center, the formally verified portion consists of the login_flow and its components login_core, lookup_target, decide_login, and issue_token, which are proven by Verus for every input.
Proof map showing how a verified login system is divided between formally proved code and trusted, tested components. Five core functions, including login_flow, login_core, lookup_target, decide_login, and issue_token, are formally verified with Verus. Supporting functions for database queries, password verification, token signing, clock access, and error handling are treated as trusted contracts that are reviewed and tested.
Proof map showing how a verified login system is divided between formally proved code and trusted, tested components. Five core functions, including login_flow, login_core, lookup_target, decide_login, and issue_token, are formally verified with Verus. Supporting functions for database queries, password verification, token signing, clock access, and error handling are treated as trusted contracts that are reviewed and tested.
Traceability diagram showing how formal verification promises are derived from requirements. Statements made by developers and decisions recorded in design cards are mapped to eight specific guarantees in the login_flow specification, covering token issuance, account roles, invalid credentials, missing accounts, malformed requests, and error handling.
Flowchart showing the end-to-end login process. A login request selects an account table based on an email or username, looks up the account, verifies the password, and issues a signed token when authentication succeeds. Error paths return appropriate HTTP responses: 400 for missing credentials, 401 for invalid credentials or missing accounts, and 500 for lookup or password-hash failures.
Diagram comparing how formal verification applies to synchronous and asynchronous functions. For both types, preconditions are checked when the function is called and postconditions are guaranteed when a result is returned. In an asynchronous login flow, the function may pause while awaiting a database lookup, and the specification makes no guarantee about whether or how quickly the operation completes.
