Programadores escrevem cada vez mais especificações formais e deixam os LLMs implementá-las, com cada implementação provada como correspondente à sua especificação. Levado a esse extremo, as linguagens de especificação tornam-se as novas linguagens de programação — mas um problema impede a troca: dois programas podem ambos satisfazer uma especificação e ainda assim se comportarem de forma diferente, então alguém ainda precisa ler o código gerado para saber qual comportamento obteve.
A resposta do Djinnlang é uma restrição de não ambiguidade. Além de provar que sua implementação satisfaz a especificação, o LLM também deve provar que qualquer outra implementação que satisfaça a mesma especificação produziria saídas idênticas para entradas idênticas. Isso fecha a brecha: o código gerado nunca precisa ser lido e pode ser regenerado a partir da especificação a qualquer momento, e um modelo não confiável pode escrever código enquanto um verificador checa seu trabalho rigorosamente.
O arranjo torna o LLM efetivamente parte da cadeia de ferramentas do compilador. Um programa Djinnlang consiste apenas em especificações — o programador nunca escreve código executável. No lugar de um compilador tradicional, um tradutor simbólico rebaixa cada especificação para stubs e obrigações de prova em Dafny, e um harness de driver orquestra um LLM que preenche implementações e provas, tudo verificado pelo verificador Dafny.
Como evidência de que o paradigma é viável, os autores mostram que o Djinnlang é auto-hospedado: um LLM implementou o tradutor Djinnlang a partir de sua própria especificação, e a reimplementação verificou a si mesma.
Provar que a especificação é não ambígua e então deixar um LLM não confiável ser o backend do compilador
Se todas as implementações de uma especificação se comportam de forma idêntica, ler o código gerado não acrescenta nenhuma informação sobre a qual um programador pudesse agir.
Provar o determinismo limita o que o modelo pode mudar, de modo que um modelo não confiável pode escrever o código enquanto o verificador carrega a confiança.
O código verificado pode ser regenerado a partir da especificação a qualquer momento, então deixa de ser um ativo que precisa ser mantido e revisado.
Exigir a prova de não ambiguidade junto com a prova de correção custa trabalho extra ao modelo, mas converte "parece certo" em uma afirmação verificada por máquina.
Quando a geração é barata e a confiança é escassa, eleve o artefato humano um nível: faça da especificação o programa, faça do determinismo uma obrigação de prova, trate o código como um artefato de build descartável.
O artigo, submetido ao arXiv em 21 de setembro de 2026, demonstra o paradigma em múltiplos exemplos e relata auto-hospedagem: um LLM implementou o tradutor Djinnlang a partir de sua especificação e a reimplementação verificou a si mesma. Os autores enquadram o resultado como uma forma forte de controle de IA — o modelo não confiável escreve, o verificador decide.
CONFIRA AS EVIDÊNCIAS