Verificação Formal Acaba de Ganhar Comprovantes. Dois Deles. Em Uma Semana.

Nos últimos meses, nossos textos sobre governança por especificação foram pesados em argumentação. Argumentamos que especificações eram a camada de controle que faltava. Argumentamos que a adoção corporativa de SDD vinha ultrapassando a própria governança. Trouxemos as notas do Cloud Next sobre desenvolvimento orientado por spec. Argumentamos que as próprias specs de agentes eram artefatos de governança. O que faltava era código rodando para apontarmos e dizer: “é assim que a espinha de verificação aparece quando alguém de fato a constrói.”

Em uma semana, ganhamos dois exemplos.

A Antfly publicou um workflow de cinco passos em que agentes de IA escrevem specs em TLA+, rodam o model checker contra um key/value store de nível de produção e expõem uma race condition real. Reuben Brooks publicou o Shen-Backpressure, um compilador que transforma definições de tipo em cálculo de sequentes em guard types selados para Go, TypeScript, Python e Rust, recusando código de agente inválido em tempo de compilação. Camadas de abstração diferentes. Linguagens diferentes. Mesma tese de fundo: quando geração de código é barata, verificação precisa ser estrutural, não opcional.

Este texto não é uma re-argumentação. O padrão deixou de ser hipotético. O texto é: como cada um dos dois stacks se parece, e o que eles dizem sobre o destino da espinha de verificação.

O Que a Antfly Fez

O texto de Rowan Copley, Cheap Code Means Formal Verification Is Reasonable Now, pega um workflow que a maioria dos times de engenharia classificaria como “acadêmico” e o coloca para rodar contra o Pebble, o key/value store que sustenta o Cockroach Labs. O time escolheu uma race condition histórica do Pebble como benchmark e perguntou: um workflow TLA+ guiado por agente consegue achar esse bug sem conhecimento prévio?

A resposta foi sim, e o workflow que produziu a resposta tem cinco passos:

1. Escrever um assumptions.md e um boundaries.md que descrevem o que é o sistema e o que a verificação está autorizada a tocar.
2. O agente escreve as specs em TLA+, roda o model checker e reporta achados.
3. Validar os achados contra o código real.
4. Criar testes unitários que reproduzem o bug no código de produção.
5. Corrigir o bug e documentar o resultado para personas de stakeholders.

O achado principal foi a race condition. O achado mais silencioso foi o loop de otimização de QPS: o mesmo workflow, apontado para uma métrica em vez de uma propriedade de correção, fez hill-climbing de performance em “ordens de magnitude”. Verificação formal, nesse stack, não é só caçador de bugs. É um procedimento de busca sobre um espaço de estados definido, e o espaço de estados inclui “rápido” ao lado de “correto”.

A história de custo é a parte que muda a conversa. TLA+ existe há décadas. Times de engenharia não adotaram em larga escala porque o investimento inicial para escrever a spec era maior do que o valor esperado de encontrar o bug. Quando o autor da spec é um agente operando a partir de um assumptions.md, o custo da verificação formal desaba. A decisão deixa de ser “esse bug vale uma semana de TLA+”. A decisão passa a ser “esse subsistema vale uma rodada no loop de verificação”. A resposta vira sim com muito mais frequência.

O Que Reuben Brooks Fez

O texto de Reuben Brooks, Structural Backpressure Beats Smarter Agents, ataca o problema de verificação uma camada abaixo. Onde a Antfly captura bugs de concorrência via model checking, Brooks captura bugs de autorização (e dezenas de outros erros de forma de estado) via tipos. O veículo é Shen, um Lisp estaticamente tipado com tipos em cálculo de sequentes, usado para gerar guard types selados em linguagens-alvo.

O exemplo do post é direto. Um agente escreve uma função em Go que usa um tenant ID sem passar pelo gate de autorização. O compilador recusa:

cannot use tenantID (variable of type string) as shenguard.TenantId

O agente não precisou ser mais inteligente. O compilador recusou a forma do valor que o agente produziu. A formulação de Brooks é que o loop em torno do agente tem cinco gates por iteração do sb CLI dele:

1. Geração de spec via shengen.
2. Testes.
3. Compilação.
4. Type-check de Shen.
5. Scripts de auditoria.

A frase que importa: gates estruturais “produzem respostas definitivas dentro do escopo, operando independentemente da capacidade do modelo”. Tradução: o gate não fica mais inteligente quando o modelo fica mais inteligente, e não fica mais burro quando o modelo fica mais burro. Produz a mesma resposta para a mesma entrada. Essa é a propriedade que faz uma espinha de verificação.

É o mesmo princípio que o workflow TLA+ da Antfly codifica em outra camada. O model checker acha um contraexemplo ou não acha. A saída não depende de qual agente o rodou.

Duas Camadas, Uma Arquitetura

Empilhe as duas peças e a foto aparece.

Na camada de spec, a Antfly tem agentes escrevendo specs em TLA+ a partir de um assumptions.md restrito. O model checker é o gate. A saída é um trace de contraexemplo ou uma execução limpa. O trabalho do agente é compor a spec, não ser confiado com o veredito.

Na camada de tipo, Brooks tem agentes emitindo código em linguagens-alvo. O compilador é o gate. A saída é uma recusa ou um build que passa. O trabalho do agente é produzir código que satisfaça os tipos, não ser confiado com a segurança.

Camadas diferentes. Mesma arquitetura. O agente é a mão de obra; o verificador é o piso. O verificador não precisa entender intenção. Precisa recusar a forma errada.

É o que vimos apontando há meses. O déficit de governança no SDD corporativo foi a descrição do piso ausente. Specs de agentes como artefatos de governança foi a descrição da mão de obra ausente. As duas peças desta semana são montagens funcionais, em famílias de linguagem diferentes, em camadas de abstração diferentes, com técnicas de verificação diferentes. Não são acadêmicas. O workflow da Antfly reproduziu um bug real do Pebble. O compilador de Brooks recusa código real em Go. Os comprovantes estão na mesa.

O Que Isso Diz Sobre os Próximos Doze Meses

Se você estava esperando o padrão “verificação formal mais agentes” sair da palestra de conferência e entrar no codebase, a espera acabou. Dois praticantes entregaram implementações funcionais na mesma semana. Não serão os últimos. O padrão é limpo demais e a economia de custo favorável demais para o próximo lote de times ignorar.

Três implicações se seguem.

Primeiro, o verificador vira o diferencial. Se dois patches gerados por agentes compilam e passam nos testes, mas apenas um passa numa rodada de model checker, a rodada de model checker é o que permite o deploy. O time com a espinha de verificação entrega mais rápido do que o time sem ela, porque o time sem a espinha ainda precisa descobrir o bug em produção.

Segundo, a spec vira ativo. assumptions.md e boundaries.md não são prompts descartáveis. São o contrato de verificação de um subsistema e vivem enquanto o subsistema viver. Times que escrevem bem acumulam uma biblioteca de superfícies verificáveis. Times que não escrevem, não acumulam.

Terceiro, a camada de abstração está em aberto. A Antfly opera na camada de design de sistema. Brooks opera na camada de sistema de tipos. Nada impede um próximo time de operar na camada SQL (validação em tempo de compilação de schema contra migrations emitidas por agente), na camada de contrato de API (recusando handlers HTTP gerados por agente que violam schemas publicados) ou na camada de política (recusando ações de agente que violam contratos de IAM antes de chegarem ao runtime). O padrão viaja.

Faça Isto Agora

Escolha um subsistema do codebase em que uma resposta errada sairia cara. Escreva o assumptions.md dele: o que é, do que depende, quais invariantes precisam valer. Escreva o boundaries.md: o que a verificação pode tocar, o que está proibida de mudar.

Agora pergunte: qual dos dois stacks serve ao seu subsistema? Se o modo de falha é concorrência ou deriva de máquina de estado, o workflow TLA+ da Antfly é o ponto de partida. Se o modo de falha é acesso não autorizado, forma de dado não confiável ou autorização pulada, o padrão Shen-Backpressure de Brooks é o ponto de partida. Rode uma iteração do loop. Veja o que o verificador recusa.

Os comprovantes estão na mesa. A espinha de verificação não é mais teórica. Construa o piso antes que seus agentes precisem dele.

---

Fontes

• Antfly. “Cheap Code Means Formal Verification Is Reasonable Now.” Maio de 2026.
• Reuben Brooks. “Structural Backpressure Beats Smarter Agents.” Maio de 2026.

A Victorino ajuda times de engenharia a adicionar espinhas de verificação estrutural aos workflows de agentes: contato@victorino.com.br | www.victorino.com.br