Métodos formais nunca falharam por ser ideia ruim. todo mundo sabia que era o santo graal, só que a chave custava 69 doutores-mês para cada 4200 linhas de código. Agora o custo despencou pra zero, e quando o custo de uma obviedade tende a zero não tem debate, tem inevitabildiade.

Daqui a pouco tem estagiário empurrando prova de refinamento pra produção sem saber o que é uma tripla de hoare do mesmo jeito que hoje empurra container sem saber o que é cgroup, e por isso vai funcionar.

Mas o futuro não é simplesmente “o modelo escreveu uma prova em Lean, compilou, acabou”. Isso prova que a prova está correta. Não prova que formalizou o problema certo. Se o requisito tá torto você ganha um certificado de excelência matemática pra sua cagada. Parabéns.

O futuro é o famigerado spec-driven development levado às últimas consequências.

Você escreve uma intenção ambígua, porque aparentemente foi para isso que a civilização inventou a escrita. Um agente transforma aquilo em linguagem natural controlada. Outro extrai uma especificação formal, gera contratos, invariantes e propriedades temporais. Outro refina isso em máquinas de estado e arquitetura. Outro finalmente gera código. E se você for insano o suficiente, o último faz logo o RTL, por até a CPU vai ser coisa obsoleta em breve. Em cada passagem, o nível inferior vem acompanhado da prova matemática que refina o superior corretamente. E aí podemos finalmente dizer a frase proibida:

Você não precisa revisar o código gerado.

E quando uma prova falha, o erro não vai morrer lá embaixo como 14 páginas de símbolos incompreensíveis produzidas pelo Lean ou pelo SMT solver. Ele sobe como calor. Cada nível preserva origem, contexto e justificativa atravessando toda a compilação. Até que o absurdo técnico encontrado a cinco níveis de profundidade reapareça para o humano como um diagnóstico mundano:

requirements/braking.md:47: a expressão “o sistema deve responder rapidamente” não define um limite de tempo suficiente para provar a propriedade de segurança.

Você corrige uma frase mal escrita no Markdown e manda compilar o sistema inteiro outra vez. E é por isso que a profissão não acaba. Alguém ainda tem que dizer o que caralhos quer. Era isso o trabalho o tempo inteiro, você só não tinha percebido por que estva ocupado escrevnedo código.

No fim, o código-fonte vira apenas mais um IR. Um artefato intermediário feio, enorme e descartável que nenhum ser humano deveria perder tempo lendo ou escrevendo, exatamente da mesma forma que aconteceu com o assembly. Não porque a IA ficou confiável. Porque finalmente construímos um pipeline baseada na premissa correta de que ela não merece confiança.

E eu realmente não sei por que ainda não existem dez mil skills fazendo isso. A teoria está escrita há décadas. Os velhos sábios deixaram tudo documentado enquanto o restante da indústria discutia se precisava mesmo escrever requisito antes da sprint.

Então vá ler Rigorous Software Development e Formal Methods for Software Engineering, transforme 60 anos de ciência da computação ignorada numa esteira de agentes e lance isso como “Formal Vibes” numa landing page com gradiente roxo e fique bilionário. Esquece o Lean. Lean é bonito, tem hype, mas quem tem compilador verificado de ponta a ponta é o Coq.

Enquanto qualquer wrapper de API com quatro prompts e um README.md escrito pelo ChatGPT explode no GitHub, CertiRocq e CompCert continuam lá, pegando poeira, contendo algumas das peças mais valiosas já produzidas pela ciência da computação. Então aponta seu agente para aqueles repositórios, manda ele construir o front-end de Markdown para Gallina, chama o resultado de Rocqstar e colete seu cheque.