Los programadores escriben cada vez más especificaciones formales y dejan que los LLM las implementen, con cada implementación demostrada como conforme a su especificación. Llevado a ese extremo, los lenguajes de especificación se convierten en los nuevos lenguajes de programación, pero un problema bloquea el cambio: dos programas pueden satisfacer una especificación y aun así comportarse de forma distinta, por lo que alguien sigue teniendo que leer el código generado para saber qué comportamiento obtuvo.
La respuesta de Djinnlang es una restricción de no ambigüedad. Además de demostrar que su implementación satisface la especificación, el LLM también debe demostrar que cualquier otra implementación que satisfaga la misma especificación produciría salidas idénticas con entradas idénticas. Eso cierra el resquicio: el código generado nunca necesita ser leído y puede regenerarse a partir de la especificación en cualquier momento, y un modelo no confiable puede escribir código mientras un verificador comprueba rigurosamente su trabajo.
El arreglo convierte efectivamente al LLM en parte de la cadena de herramientas del compilador. Un programa Djinnlang consta únicamente de especificaciones: el programador nunca escribe código ejecutable. En lugar de un compilador tradicional, un traductor simbólico reduce cada especificación a stubs de Dafny y obligaciones de prueba, y un arnés controlador orquesta un LLM que completa implementaciones y pruebas, todo verificado por el verificador de Dafny.
Como evidencia de que el paradigma es viable, los autores muestran que Djinnlang se autoaloja: un LLM implementó el traductor de Djinnlang a partir de su propia especificación, y la reimplementación se verificó a sí misma.
Demostrar que la especificación es inequívoca y luego dejar que un LLM no confiable sea el backend del compilador
Si todas las implementaciones de una especificación se comportan de forma idéntica, leer el código generado no aporta información sobre la que un programador pueda actuar.
Demostrar el determinismo acota lo que el modelo puede cambiar, de modo que un modelo no confiable puede escribir el código mientras el verificador asume la confianza.
El código verificado puede regenerarse a partir de la especificación en cualquier momento, por lo que deja de ser un activo que deba mantenerse y revisarse.
Exigir la prueba de no ambigüedad junto con la prueba de corrección le cuesta al modelo trabajo adicional, pero convierte "parece correcto" en una afirmación comprobada por máquina.
Cuando la generación es barata y la confianza escasa, eleva un nivel el artefacto humano: haz que la especificación sea el programa, haz del determinismo una obligación de prueba, trata el código como un artefacto de compilación desechable.
El artículo, enviado a arXiv el 21 de septiembre de 2026, demuestra el paradigma en múltiples ejemplos y reporta el autoalojamiento: un LLM implementó el traductor de Djinnlang a partir de su especificación y la reimplementación se verificó a sí misma. Los autores enmarcan el resultado como una forma fuerte de control de la IA: el modelo no confiable escribe, el verificador decide.
CONSULTA LAS PRUEBAS