O PDD Kit é um protótipo de pesquisa da Microsoft Research que transforma requisitos de desenvolvimento em especificações formais e verifica código Rust escrito por agentes. No exemplo do Pet Store, publicado em 5 de novembro de 2026, a equipe relata provas para cinco funções do fluxo de login, cada uma conforme seu contrato formal. O resultado cobre essas funções e as propriedades especificadas, não toda a aplicação. Microsoft Research
O que a prova cobre no login do Pet Store
Verificação formal é uma prova matemática checada por máquina de que um programa satisfaz propriedades definidas numa especificação, para as entradas representadas pelo modelo. A Microsoft Research relata que o PDD Kit verificou login_flow, login_core, lookup_target, decide_login e issue_token. O contrato de login_flow tem oito cláusulas ensures, que descrevem condições como a relação entre conta, senha e token, além de respostas de erro.
O Pet Store é uma aplicação Rust de ponta a ponta, com cerca de 5 mil linhas. A demonstração se concentra na lógica de login. Uma prova das cinco funções não equivale a provar a loja inteira, nem outras propriedades que não estejam nos contratos.
Como a intenção vira um contrato formal
O fluxo descrito começa com requisitos em linguagem natural. A equipe esclarece ambiguidades com decisões revisadas por pessoas, converte os requisitos aprovados em contratos para o Verus e verifica se o código os cumpre. A análise também procura lacunas na especificação.
Um exemplo mostra por que a formulação importa: dizer apenas que uma senha correta é necessária para emitir um token também permitiria um sistema que recusasse todos os logins. O contrato mais completo exige que a senha correta resulte em token, salvo falha na consulta ou na assinatura; uma senha incorreta, quando o hash pode ser lido, leva a uma recusa, salvo falha na consulta. Se o hash armazenado não puder ser lido, o exemplo prevê um erro interno.
O cartão de decisão apresenta as duas formulações: provar apenas que não há token sem a senha correta ou exigir também que a senha correta produza um token. A segunda condição elimina a possibilidade de um login que sempre recusa o usuário.
Ao avaliar uma prova, confira primeiro quais comportamentos o contrato exige. O verificador pode demonstrar que o código cumpre essas regras; a escolha das regras continua sendo uma decisão de projeto.
O que fica sob confiança e testes
Parte do fluxo depende de operações externas que o exemplo trata como confiáveis. A Microsoft Research descreve seis categorias de aprovação; uma delas agrupa duas consultas ao banco de dados. Entre as dependências estão as consultas, a verificação de senha com bcrypt, a assinatura de tokens, o relógio, o tratamento de erros do banco e a extração dos dados da requisição. Os contratos dessas operações são aceitos e testados, mas as implementações externas não são provadas pelo Verus nesse exemplo.
A diferença prática é que uma prova abrange as propriedades definidas no modelo, enquanto um teste exercita casos específicos. Um token de exemplo deve expirar 86.400 segundos após a leitura do relógio; o contrato da função de relógio é uma premissa confiável, não uma prova do comportamento do relógio real. O contrato assíncrono também descreve os resultados caso a operação retorne, mas não garante que o login termine nem quanto tempo levará.
Por que a especificação ainda precisa de revisão
Uma prova pode confirmar que o código segue uma especificação incompleta ou equivocada. O processo de revisão do PDD Kit ajuda a explicitar decisões e encontrar cláusulas fracas, mas não demonstra que todos os requisitos pretendidos foram capturados.
No artigo de 17 de março de 2026, Shuvendu K. Lahiri situa testes e contratos executáveis numa faixa mais leve de formalização, contratos lógicos como os do Verus numa etapa mais rigorosa e a síntese verificada por linguagens específicas de domínio (DSLs) num extremo ainda mais ambicioso. O trabalho aponta a validação da especificação como um desafio central: não há uma medida independente que represente por completo a intenção de quem desenvolve. Artigo de Shuvendu K. Lahiri
Por que o Verus torna o exemplo específico de Rust
A Microsoft Research descreve o protótipo do PDD Kit como compatível apenas com Rust. O Verus, ferramenta usada na demonstração, verifica programas Rust com técnicas SMT, que usam solucionadores para checar condições matemáticas. Sua descrição oficial também explica que as provas aproveitam a sintaxe de Rust, os tipos lineares e o mecanismo de empréstimo (borrow checking) para expressar propriedade e separação de recursos. Isso caracteriza o Verus; não amplia o resultado demonstrado no login do Pet Store. Projeto Verus da Microsoft Research
