Três Visões Sobre Governança de Código IA: Tipos, Especificações e Confiança Verificável

Na mesma semana de março de 2026, três autores sem nenhuma relação entre si publicaram três argumentos independentes sobre o mesmo problema. Vint Cerf e coautores escreveram na ACM Communications que confiança precisa se tornar infraestrutura para agentes de IA. Um praticante de teoria de tipos argumentou que tipos dependentes transformam o compilador em ferramenta de governança. E uma especialista em Haskell demonstrou que especificações suficientemente detalhadas inevitavelmente se tornam código.

Nenhum deles respondia ao outro. Chegaram à mesma fronteira por caminhos diferentes. Essa convergência é o sinal que merece atenção.

Vimos esse argumento se construindo desde fevereiro. Em Quando a IA Escreve o Software, Quem Define o que É Correto?, mostramos que verificação formal é governança porque especificações codificam valores. Em US$ 200M Confirmam: Verificação É Infraestrutura, documentamos o mercado validando essa tese com capital institucional. O que esses três novos textos adicionam é uma triangulação: a mesma conclusão alcançada por arquitetura de redes, teoria de linguagens de programação e engenharia de software aplicada. Três disciplinas. Uma descoberta.

Posição Um: Confiança como Infraestrutura

Mallik Tatipamula, David Attermann e Vinton Cerf publicaram “From Distributed Intelligence to Verifiable Responsibility” na ACM Communications. Cerf não é uma voz secundária aqui. Ele co-projetou o TCP/IP. Foi presidente da ACM. Quando descreve algo como requisito de infraestrutura, a afirmação carrega o peso de alguém que construiu infraestrutura usada diariamente por bilhões de pessoas.

O argumento deles: a internet nativa de IA não vai escalar apenas com inteligência distribuída. Precisa de responsabilidade distribuída, tornada executável por meio de accountability verificável. Coordenação autônoma depende da capacidade dos sistemas avaliarem a legitimidade de ações em tempo real, sem depender de intermediários centralizados ou governança retrospectiva.

Releia essa última parte. “Sem depender de intermediários centralizados ou governança retrospectiva.” É uma rejeição direta do modelo dominante de compliance, onde um humano revisa o output da IA depois do fato e decide se era aceitável. Cerf e coautores dizem que esse modelo não escala. Confiança precisa ser avaliada em tempo de execução, pela própria infraestrutura, enquanto as ações acontecem.

A analogia que traçam é estrutural. Roteamento foi a função de infraestrutura que fez a Web 1.0 funcionar. Orquestração foi a função de infraestrutura que fez a Web 2.0 funcionar. Confiança é a função de infraestrutura que fará a web nativa de IA funcionar. Ou fracassar, se ninguém a construir.

Não é uma posição teórica. É uma reivindicação arquitetural sobre o que a próxima camada de protocolo precisa fazer.

Posição Dois: Tipos São Prova

O segundo texto, “Don’t Vibe, Prove,” vem da comunidade de teoria de tipos dependentes. O autor, NGrislain, faz um argumento técnico específico: a geração de código por IA muda a proposta de valor das linguagens de programação. Quando humanos escreviam todo o código, legibilidade e expressividade importavam mais. Quando a IA escreve o código, garantias de correção importam mais. Sistemas de tipos dependentes como Lean 4 fornecem essas garantias por construção.

A demonstração é concreta. Um algoritmo de insertion sort em Lean 4 ocupa 6 linhas. A prova de que o algoritmo está correto ocupa 25 linhas. O sistema de tipos aplica invariantes em tempo de compilação: a saída está ordenada, contém exatamente os elementos da entrada, nada se perde ou se duplica. Se o código compila, está correto. Não “testado e provavelmente correto.” Provadamente correto.

A descoberta interessante aconteceu durante o processo de prova. O sistema de tipos exigiu uma prova de ordenação total sobre o tipo de entrada. É um requisito matemático que humanos podem deixar passar (e frequentemente deixam). O compilador capturou uma premissa ausente que testes provavelmente não detectariam, porque testes só verificam os casos que você pensa em escrever.

O enquadramento do autor é afiado: “A especificação É o código. Não existe distância entre a invariante e a implementação.” E sobre IA: “O ciclo de feedback adversarial que exaure programadores humanos é exatamente o ambiente onde IA se destaca.” Humanos acham o vai-e-vem de satisfazer um verificador de tipos tedioso. IA não cansa. A combinação de tipos dependentes e geração de código por IA transforma o compilador em um oráculo de verificação que nunca precisa dormir.

Isso se conecta diretamente com a história da Axiom. Quando a Axiom levantou US$ 200M para construir infraestrutura de verificação em Lean 4, o mercado estava apostando exatamente nessa dinâmica. A IA gera o código. O sistema de tipos prova que está correto. O compilador é a camada de governança.

Posição Três: Especificações Viram Código

Gabriella Gonzalez, escrevendo no Haskell for All, ataca pela direção oposta. Seu argumento: a alegação de que especificações são mais simples que implementações é falsa. Uma especificação suficientemente detalhada necessariamente se torna código.

Ela testa isso empiricamente. A OpenAI publicou o Symphony, um framework multi-agente, com um documento de especificação que tem aproximadamente um sexto do tamanho da implementação. Gonzalez aponta que a spec está incompleta. Usou o Claude Code para gerar o Symphony em Haskell a partir daquela especificação. O resultado tinha múltiplos bugs. O agente “girava silenciosamente,” produzindo output que compilava mas falhava em runtime.

Sua conclusão: “Se você tentar tornar um documento de especificação preciso o suficiente para gerar uma implementação funcional de forma confiável, você necessariamente contorce o documento em código.” A fronteira entre spec e código é uma ilusão. Conforme as especificações se tornam precisas o suficiente para serem úteis na geração de código por IA, se tornam programação em outra sintaxe.

Essa descoberta reforça o que exploramos em Quando a Especificação É o Produto, Quem Governa a Especificação?. Se a spec é a verdadeira superfície de controle, e se specs precisam alcançar precisão de código para serem úteis, então governança precisa operar com precisão de código. Não existe uma camada confortável de abstração onde stakeholders de negócio escrevem prosa em português e recebem software verificado. O problema de governança vive no mesmo nível de detalhe que o problema de implementação.

Onde as Três Posições Convergem

Cada autor provavelmente discordaria dos outros dois em pontos específicos. Cerf pensa em protocolos de rede e interoperabilidade de agentes. NGrislain pensa em correção garantida pelo compilador dentro de uma única base de código. Gonzalez pensa nos limites práticos da especificação como metodologia.

Mas convergem em um ponto. Governar sistemas gerados por IA exige restrições verificáveis por máquina que operam no nível onde o trabalho realmente acontece.

Cerf diz: verificação de confiança em tempo de execução, na infraestrutura, não depois do fato por um humano.

NGrislain diz: aplicação de correção em tempo de compilação, no sistema de tipos, não depois do fato por uma suíte de testes.

Gonzalez diz: precisão de especificação no nível de código, na linguagem formal, não depois do fato por um documento em prosa.

Os três rejeitam a mesma coisa: a crença de que governança pode operar a uma distância confortável da implementação. Revisão retrospectiva. Testes manuais. Especificações em linguagem natural. São os mecanismos que a maioria das organizações usa hoje. E os três autores, independentemente, na mesma semana, publicaram argumentos sobre por que esses mecanismos são insuficientes.

A Implicação Incômoda

Se essas três posições estão corretas (e a convergência sugere que estão), a maioria das organizações enfrenta um problema estrutural. Sua infraestrutura de governança opera no nível errado de abstração.

Políticas de IA no nível do conselho são escritas em linguagem natural. Frameworks de compliance avaliam outputs após o deploy. Revisões de segurança acontecem no momento do pull request, que é depois da geração mas antes da produção. Uma janela estreita que escala mal. Especificações vivem em páginas de Confluence que nenhum compilador jamais leu.

A alternativa que esses três textos apontam é infraestrutura de verificação embutida no próprio processo de desenvolvimento. Sistemas de tipos que rejeitam código incorreto antes de chegar a um revisor humano. Avaliação de confiança no nível de protocolo que rejeita ações não autorizadas de agentes antes de executarem. Especificações escritas em linguagens formais que uma máquina pode verificar, não prosa que um comitê pode interpretar.

Isso é mais difícil do que o que a maioria das organizações faz hoje. Exige investimento em ferramentas, treinamento e mudança de processos. Mas a alternativa é uma carga de verificação crescente sendo tratada por um grupo cada vez menor de revisores humanos qualificados. Esse caminho não escala. Cerf diz isso. A comunidade de teoria de tipos diz isso. Os engenheiros práticos dizem isso.

O Que Organizações Devem Fazer

Tratar verificação como infraestrutura, não como processo. A analogia arquitetural de Cerf é o enquadramento correto. Roteamento não é um processo que alguém executa manualmente. É infraestrutura que opera automaticamente. Verificação precisa do mesmo tratamento. Organizações que embutem verificação em suas cadeias de ferramentas (sistemas de tipos, specs formais, provas automatizadas) vão escalar o uso de IA. Organizações que dependem de revisão humana vão criar gargalos.

Avaliar sistemas de tipos dependentes para código de alta consequência. Lean 4 é o líder atual, e a aposta de US$ 200M da Axiom confirma confiança institucional. Para bibliotecas criptográficas, lógica de autorização, cálculos financeiros e sistemas de missão crítica, a proporção de 25 linhas de prova por 6 linhas de código é uma barganha comparada ao custo de uma falha em produção. Comece pelo código que seria mais caro errar.

Parar de fingir que specs e código são artefatos separados. O insight de Gonzalez evita uma armadilha comum: investir em documentos de especificação elaborados que são imprecisos demais para gerar código correto e complexos demais para manter junto com a implementação. Se você precisa de precisão formal, escreva em linguagem formal. Se precisa de flexibilidade, aceite que sua spec é um guia, não uma garantia, e invista em verificação em runtime para capturar o que a spec deixou escapar.

Construir o músculo de governança na altitude correta. O padrão em todos os três textos é que governança precisa operar onde o trabalho acontece. Para código compilado, isso significa o sistema de tipos. Para agentes em rede, significa a camada de protocolo. Para especificações, significa linguagens formais. Identifique onde vive seu código gerado por IA de maior risco e empurre a verificação para esse nível.

A convergência desses três argumentos independentes não é coincidência. Reflete um entendimento em amadurecimento sobre o que governança de IA realmente exige. Não políticas. Não comitês de revisão. Não auditorias retrospectivas. Restrições verificáveis por máquina, operando em tempo real, no nível da implementação.

As organizações que construírem essa infraestrutura vão governar seus sistemas de IA. O resto vai apenas torcer para que seus sistemas se comportem.

Fontes

Tatipamula, Attermann, Cerf. “From Distributed Intelligence to Verifiable Responsibility.” ACM Communications, março 2026.
NGrislain. “Don’t Vibe — Prove.” Março 2026.
Gonzalez, Gabriella. “A Sufficiently Detailed Spec Is Code.” Haskell for All, março 2026.

A Victorino ajuda empresas a construir infraestrutura de verificação para código gerado por IA, de governança baseada em tipos a arquiteturas de confiança verificável: contato@victorino.com.br | www.victorino.com.br