Design by Contract na Era da IA: Como os Contratos de Meyer Protegem a Criptografia Onde os Testes Falham

Design by Contract na Era da IA: Como os Contratos de Meyer Protegem a Criptografia Onde os Testes Falham

Em março de 2026, documentos internos da Anthropic sobre o modelo Claude Mythos vazaram. Semanas depois, eles mesmos o anunciaram. O Mythos encontrou um 0-day no OpenBSD que estava no código há vinte e sete anos. Vinte e sete. No FFmpeg, foi descoberto algo semelhante, com dezesseis anos, e o kernel do Linux também foi afetado. A busca por um bug no OpenBSD custou menos de cinquenta dólares de computação. O FFmpeg já havia sido escaneado milhões de vezes por ferramentas automáticas, e nada.

Tudo bem, digamos que isso seja impressionante. Mas o que fazer com isso? Proibir a IA de procurar bugs não vai funcionar. Portanto, é preciso construir sistemas de forma que os erros lógicos não cheguem à produção.

A resposta padrão é: reescrever em Rust. Para corrupção de memória, isso realmente funciona (embora não para tudo legado), o modelo de propriedade impede a compilação de use-after-free e buffer overflow, e os bugs no OpenBSD e FFmpeg eram exatamente dessa categoria. Mas aqui está a questão. Há toda uma classe de erros que nenhuma linguagem vê, e esses são erros lógicos. Escolheu o padding errado para RSA, o compilador fica em silêncio. Esqueceu de verificar a revogação do certificado ou passou entropia bruta para DRBG sem verificar a qualidade, os testes são verdes. Porque ninguém escreveu um teste para isso.

Os testes geralmente verificam exatamente o que o programador pensou em verificar. A vulnerabilidade no OpenBSD passou em todos os testes por vinte e sete anos. Todos eles. É preciso uma abordagem que funcione não no nível da sintaxe, mas no nível das garantias arquiteturais. Que fixa “o que o sistema deve fazer” antes da primeira linha de código. Não “como implementar”, mas “o que garantir”. A diferença é fundamental: a implementação pode ser reescrita, mas a garantia ou é cumprida ou não.

Historicamente, essa abordagem já foi inventada. Em 1986. Autor: Bertrand Meyer. Design by Contract. E há uma razão específica pela qual você provavelmente não ouviu falar disso.

Mais adiante: por que o DbC não decolou, o que um agente de IA muda e como isso se parece em um sistema PKI real com um repositório aberto.

DbC de Meyer: Por que não decolou

A ideia é simples. Cada módulo declara explicitamente três coisas: o que espera na entrada (pré-condições, PRE), o que garante na saída (pós-condições, POST), o que nunca violará (invariantes, INV). Por exemplo, a função de divisão: PRE: divisor ≠ 0, POST: resultado × divisor == dividendo. Simples, mas formal.

Estrito. Formal. E não pegou no mainstream, o que, em geral, é previsível.

A razão é banal: trabalho em dobro. Na prática, parece assim: primeiro você escreve o contrato. Então você escreve o código. Então você escreve os testes. O contrato é uma carga adicional que não dá retorno imediato. Quando o prazo está apertado, os contratos são jogados fora primeiro.

Em áreas críticas para a segurança, o DbC sobreviveu. Ada/SPARK na aviação, ISO 26262 na indústria automotiva. Essencialmente, os mesmos PRE/POST/INV, apenas com outros nomes e outro orçamento. Lá, o preço do erro é tal que o trabalho em dobro é justificado. No desenvolvimento normal: não. E todos entenderam isso.

Eiffel, a linguagem de Meyer com contratos embutidos, permaneceu de nicho. Microsoft Code Contracts para C#: abandonado. Java adicionou assert em 1.4, mas sem obrigatoriedade. A linguagem D incorporou contratos na sintaxe e também não se tornou mainstream. A ideia se espalhou por asserts, anotações, tipos. Mas PRE/POST/INV formais no nível da arquitetura nunca se tornaram a norma.

Por 40 anos, o DbC esperou o momento em que a segunda metade do trabalho pudesse ser entregue a outra pessoa. E parece que esse momento chegou.

Aliás, não fui o único a notar isso. Nos últimos anos, houve trabalhos acadêmicos na interseção de DbC e LLM. “A DbC Inspired Neurosymbolic Layer for Trustworthy Agent Design” (arxiv:2508.03665): uma camada contratual entre o LLM e a saída. “Formal Specification and Runtime Enforcement for Reliable Autonomous AI Agents” (arxiv:2602.22302): ABC-contratos para agentes de IA. Fun2spec (openreview): LLM gera contratos para milhões de linhas de C/C++. Em blogs, eles escrevem sobre “prompt contracts” e “files as contracts”.

Mas todos esses trabalhos: ou são teoria sem prova de produção, ou engenharia de prompt sem PRE/POST/INV formais. A combinação “DbC + agente de IA + criptografia + repositório aberto” ainda não foi mostrada por ninguém. Eu estava interessado em tentar.

O que um agente de IA muda

A pessoa escreve o contrato. O agente pega e escreve o código, os testes, as verificações. E a pessoa então olha para 10 linhas de contrato em vez de mil linhas de implementação e decide se tudo está correto.

Na verdade, é isso. O agente assume a implementação e a geração de testes, e o trabalho em dobro que matou o DbC desaparece. O contrato permanece a única tarefa da pessoa.

Na prática, um ciclo é assim. Escrevo um invariante: “PKCS#1 v1.5 == PROIBIDO”. O agente gera crypto_engine.py com RSA-PSS. Paralelamente, gera um teste de contrato que tenta chamar PKCS#1 v1.5 e verifica se o sistema o rejeita. O teste passou, o contrato foi cumprido. Falhou: o agente corrige a implementação, não o contrato. Contrato: fonte da verdade. Não o tocam.

Um erro no contrato também é possível, é claro. Mas, em um caso típico, verificar 10 linhas de declaração de intenção, especialmente se você estiver verificando com NIST ou RFC, é mais fácil do que procurar um erro lógico em 1000 linhas de implementação. O contrato é um ponto focal. Em vez da pergunta “o código está escrito corretamente?”, você responde à pergunta “descrevi corretamente o que quero?”. A segunda pergunta é mais fácil.

Prova: PKI com TRNG de hardware

Eu construí um sistema PKI com um gerador de números aleatórios de hardware e quero contar como foi. O objetivo do caso é mostrar que DbC + agente de IA funciona não na teoria, mas em um projeto embarcado fullstack real com criptografia. De ponta a ponta. Na entrada, ruído térmico do ADC do microcontrolador. Ele vai para DRBG de acordo com NIST SP 800-90A, de lá para a geração de chaves, então a CA emite um certificado X.509. O desenvolvimento foi feito no Windows, a produção roda no Linux ARM64 (RK3328, Cortex-A53), e o firmware vive no STM32.

A pilha é assim: STM32G431 remove ruído térmico do ADC interno e entrega entropia bruta via USB HID. No host (RK3328), um daemon Python lê esses bytes, passa por uma verificação de integridade de acordo com NIST 800-90B e os alimenta no HMAC-DRBG. Em seguida, o CryptoEngine pega a saída do DRBG e gera chaves RSA/ECDSA. KeyStorage criptografa chaves privadas AES-256-GCM e as coloca no disco. O serviço CA assina certificados. Cinco módulos, cada um com seu próprio contrato na interface.

Aqui estão os números. O principal aqui: duas vulnerabilidades CRITICAL foram encontradas precisamente através da abordagem contratual, antes da produção.

O repositório está aberto: github.com/vasilievsv/hw.pki-on-box

SELinux em execução, filtros eBPF, sandboxing do systemd, tudo como deveria ser. Sobre o firmware: 12 pontos de auditoria criptográfica de acordo com NIST 800-90B, todos os 12 fechados, zero abertos.

O desenvolvimento ocorreu em várias fases. Primeiro, a auditoria do protótipo e a escrita de contratos para cada módulo. Em seguida, a implementação do core: TRNG, DRBG, CryptoEngine, KeyStorage, serviço CA, CRL. Paralelamente, testes de contrato, primeiro em mocks (62 testes), depois em hardware real (15 testes HW). Uma fase separada no firmware: três placas STM32, novo firmware para G431, 12 pontos de auditoria criptográfica. E o final: implantação no RK3328, reconstrução do kernel 5.10 com SELinux e eBPF, testes de fumaça no hardware real. Cada fase é uma sessão separada com o agente, com seu próprio papel e contexto. Os papéis são importantes: o testador não escreve código, o codificador não altera os contratos, o arquiteto não executa os testes. Isso não é burocracia, é uma maneira de impedir que o agente se desvie. Quando a sessão tem um papel e um contrato, o agente trabalha dentro da estrutura. Sem estrutura, ele começa a “ajudar” e quebra o que já está funcionando.

Dois contratos em duas interfaces

Toda a criptografia em pki-on-box é baseada em dois contratos, e cada um deles fecha uma interface arquitetural. As interfaces foram escolhidas não por acaso: é nas fronteiras dos módulos que erros lógicos surgem, que não são visíveis dentro do módulo. DRBG entrega bytes, CryptoEngine os usa. Se você não fixar qual padding é permitido nesta interface, o erro é inevitável. Abaixo, versões simplificadas para ilustração, contratos completos no repositório.

Primeiro, a geração de chaves:

yaml
contract: key_generation
  PRE:
    - DRBG.seeded == true
    - DRBG.reseed_counter < max_requests
    - algorithm ∈ {RSA-2048, RSA-4096, ECDSA-P384, Ed25519}
  POST:
    - private_key.encrypted(AES-256-GCM)
    - nonce.unique()
    - public_key = derive(private_key)
  INV:
    - padding == RSA-PSS (assinatura) | RSA-OAEP (cifração)
    - PKCS#1 v1.5 == PROIBIDO

Por que PKCS#1 v1.5 é proibido. Não é um capricho. O ataque Bleichenbacher (1998) usa um oracle de padding em PKCS#1 v1.5 para restaurar o texto simples. Este não é um ataque teórico, ele foi usado em sistemas reais. RSA-PSS e RSA-OAEP são projetados para que essa classe de ataques seja impossível. O invariante no contrato fecha isso no nível da arquitetura. Antes que alguém escolha acidentalmente v1.5 “porque foi assim no exemplo do StackOverflow”.

O segundo contrato, emissão de certificado:

yaml
contract: certificate_issuance
  PRE:
    - issuer_ca.valid() && !issuer_ca.revoked()
    - csr.signature.verify() == true
  POST:
    - cert.serial.unique()
    - cert.signature.verify(issuer_ca.public_key) == true
    - cert.extensions.key_usage.set()
  INV:
    - cert_chain.depth <= max_path_length
    - root_ca.offline == true (air-gapped)

A verificação automática por meio de testes de contrato encontrou dois problemas CRITICAL: padding incorreto (PKCS#1 v1.5 em vez de RSA-PSS) e modo AES incorreto.

Por que os testes normais ignoram isso? Ambos são erros lógicos, e nem o compilador nem o linter são úteis aqui. Testes unitários normais podem ter pego, mas para isso alguém teria que ter adivinhado escrevê-los. E os testes de contrato são gerados a partir da especificação formal. Eles não precisam que o programador adivinhe alguma coisa.

Implementação:

test_crypto_engine_contract.py

Veja como um dos testes invariantes se parece no código:

python
class TestCryptoEngineInvariants:

    def test_rejects_pkcs1v15_padding(self, crypto):
        priv, pub = crypto.generate_rsa_keypair(bits=2048)
        data = b"invariant check"
        sig = crypto.sign_data(priv, data)
        # PSS deve funcionar
        pub.verify(sig, data, padding.PSS(
            mgf=padding.MGF1(hashes.SHA256()),
            salt_length=padding.PSS.AUTO
        ), hashes.SHA256())
        # PKCS1v15 deve quebrar
        with pytest.raises(Exception):
            pub.verify(sig, data, padding.PKCS1v15(), hashes.SHA256())

O teste não verifica “se a assinatura funciona”. Ele verifica o invariante do contrato: o sistema assina RSA-PSS, e PKCS#1 v1.5 deve quebrar na verificação. Se alguém mudar o padding por engano, este teste falhará. Não porque o programador adivinhou, mas porque o contrato exigiu.

Como funciona

O processo não é linear, mas, para simplificar, é mais ou menos assim.

Primeiro, formulo o contrato, PRE/POST/INV na interface dos módulos. Para mim, esta é a parte mais difícil, porque você tem que se forçar a pensar não no código, mas nas garantias: o que o sistema deve fazer, o que é proibido para ele.

Na prática, parece assim. Abro uma nova sessão, especifico o papel (codificador, testador, arquiteto), carrego o contexto do trabalho anterior. Escrevo o contrato em yaml: PRE, POST, INV. Às vezes, o contrato nasce em cinco minutos, se a interface for clara. Às vezes, fico meia hora, porque não consigo formular o invariante. Isso é normal. Se você não consegue escrever a garantia em uma linha, significa que ainda não entende o que o sistema deve fazer.

Em seguida, o agente pega esse contrato e gera a implementação, e, ao mesmo tempo, também testes de contrato, cada um dos quais verifica uma pós-condição específica ou tenta violar o invariante.

O teste falhou, o agente corrige a implementação. Não toca no contrato. Eu só altero o contrato, e somente se entender que cometi um erro na especificação. A violação do contrato não é um aviso nem um TODO, é uma parada completa. O código não é mesclado até que todas as pós-condições estejam verdes.

Um exemplo específico. No contrato key_generation, há INV: padding == RSA-PSS. O agente gerou CryptoEngine, e a primeira versão de sign_data() usou PKCS1v15. O teste de contrato test_rejects_pkcs1v15_padding imediatamente pegou a violação: a verificação via PSS falhou porque a assinatura foi criada com outro padding. O agente reescreveu sign_data() para PSS, os testes ficaram verdes. Todo o ciclo: o contrato já estava lá, o teste já estava lá, a pessoa não participou. Eu vi a execução verde no log e fui em frente.

No pki-on-box, todo esse ciclo levou 52 sessões com o agente (sessão = um bate-papo com uma função e uma tarefa), totalizando 1780₽ em computação. Embarcado, DevOps e cripto ao mesmo tempo, uma pessoa. Sem o agente e os contratos, eu teria reservado 60+ horas, e isso é otimista. Três domínios (firmware, backend, infra), três sistemas operacionais (Windows para desenvolvimento, Linux ARM64 para produção, bare metal para MCU). Os contratos formalizam as expectativas com antecedência, e o agente as implementa sem desvios. Não há necessidade de explicar a ele pela segunda vez por que PKCS#1 v1.5 não é permitido. Isso está escrito no INV.

Limitações e ressalvas honestas

Não funciona com todos os modelos. O modelo deve manter restrições formais ao longo de uma longa sessão e não esquecer os invariantes na quinquagésima mensagem no bate-papo. Os modelos de fronteira lidam com isso. Os locais em 7B de parâmetros ainda não estão funcionando, mas é uma questão de tempo.

O contrato também pode ser escrito incorretamente, e é importante entender isso. Se você esquecer de proibir o modo CBC para AES no INV e deixar apenas GCM, o agente implementará obedientemente o CBC, e formalmente o contrato será cumprido. O contrato não substitui a experiência. Ele formaliza o que você já sabe. Se você não sabe, não há nada para formalizar. No pki-on-box, me peguei duas vezes com o contrato incompleto: uma vez esqueci o modo AES (peguei na revisão), a segunda vez não especifiquei o comprimento mínimo da semente de entropia para DRBG. Ambas as vezes, a correção do contrato levou uma linha, mas sem ele o agente teria gerado um código formalmente correto, mas vulnerável.

DbC não é uma bala de prata. Ele fecha erros lógicos em interfaces arquiteturais, e somente. Corrupção de memória é para Rust, condições de corrida são para o modelo de memória, cadeia de suprimentos é para ferramentas completamente diferentes. E mais: os contratos funcionam no nível dos módulos, não no nível de funções individuais. Escrever PRE/POST para cada getter é sem sentido. O contrato faz sentido onde há uma interface arquitetural e o preço do erro é alto.

Conclusão

Meyer inventou o Design by Contract há quarenta anos. A ideia era boa, mas o momento não era certo, e o trabalho em dobro matou a adoção.

Agora, em 2026, a IA está assumindo a segunda metade desse trabalho. A pessoa formula o contrato, e o agente implementa e verifica. O que antes era “muito caro” se transformou em “a única coisa que você precisa fazer”.

Eu consegui 131 commits em 11 dias, $129 em hardware, 1780₽ em computação. E duas CRITICAL, que foram encontradas precisamente através da abordagem contratual, antes da produção.

Mythos mostrou que a IA quebra mais rápido do que as pessoas consertam. A linguagem não salva de erros lógicos, e os testes verificam apenas o que o programador pensou. Os contratos funcionam de forma diferente: eles fixam o que o sistema deve garantir. Alguém pensou em escrever um teste ou não.

Quarenta anos atrás, Meyer se ofereceu para registrar essas garantias explicitamente. Então custou muito caro. Agora, a segunda metade do trabalho é assumida pelo agente, e o contrato permanece o único artefato pelo qual a pessoa é responsável. Dez linhas de yaml em vez de mil linhas de código.

Se você tiver criptografia, lógica de pagamento ou qualquer outro código em seu projeto onde um erro na lógica seja mais perigoso do que um erro na memória, tente escrever um contrato na interface mais crítica. PRE/POST/INV, dez linhas. Deixe o agente implementar e gerar testes. Veja o que ele encontrará.

Referências

• Meyer B. “Object-Oriented Software Construction” (1988, 2nd ed. 1997)
• Meyer B. “Applying Design by Contract” (IEEE Computer, 1992)
• Bleichenbacher D. “Chosen Ciphertext Attacks Against Protocols Based on the RSA Encryption Standard PKCS#1” (CRYPTO 1998)
• NIST SP 800-90A: Recommendation for Random Number Generation Using Deterministic Random Bit Generators
• NIST SP 800-90B: Recommendation for the Entropy Sources Used for Random Bit Generation
• “A DbC Inspired Neurosymbolic Layer for Trustworthy Agent Design” arxiv:2508.03665
• “Formal Specification and Runtime Enforcement for Reliable Autonomous AI Agents” arxiv:2602.22302
• Fun2spec: Code Contract Synthesis At Scale openreview
• Testes de contrato: test_crypto_engine_contract.py
• pki-on-box: github.com/vasilievsv/hw.pki-on-box