Les programmeurs écrivent de plus en plus des spécifications formelles et laissent les LLM les implémenter, chaque implémentation étant prouvée conforme à sa spécification. Poussé à cet extrême, les langages de spécification deviennent les nouveaux langages de programmation — mais un problème bloque ce basculement : deux programmes peuvent tous deux satisfaire une spécification et néanmoins se comporter différemment, si bien que quelqu'un doit encore lire le code généré pour savoir quel comportement il a obtenu.
La réponse de Djinnlang est une contrainte de non-ambiguïté. En plus de prouver que son implémentation satisfait la spécification, le LLM doit également prouver que toute autre implémentation satisfaisant la même spécification produirait des sorties identiques sur des entrées identiques. Cela ferme la faille : le code généré n'a jamais besoin d'être lu et peut être régénéré à partir de la spécification à tout moment, et un modèle non fiable peut écrire du code tandis qu'un vérificateur contrôle étroitement son travail.
Cet agencement fait effectivement du LLM une partie de la chaîne d'outils du compilateur. Un programme Djinnlang ne consiste qu'en spécifications — le programmeur n'écrit jamais de code exécutable. À la place d'un compilateur traditionnel, un traducteur symbolique abaisse chaque spécification en stubs Dafny et en obligations de preuve, et un harnais pilote orchestre un LLM qui remplit les implémentations et les preuves, le tout vérifié par le vérificateur Dafny.
Comme preuve que ce paradigme est réalisable, les auteurs montrent que Djinnlang est auto-hébergé : un LLM a implémenté le traducteur Djinnlang à partir de sa propre spécification, et la réimplémentation s'est vérifiée elle-même.
Prouver que la spécification est non ambiguë, puis laisser un LLM non fiable servir de backend au compilateur
Si toutes les implémentations d'une spécification se comportent de manière identique, lire le code généré n'apporte aucune information sur laquelle un programmeur pourrait agir.
Prouver le déterminisme borne ce que le modèle peut changer, de sorte qu'un modèle non fiable peut écrire le code tandis que le vérificateur porte la confiance.
Le code vérifié peut être régénéré à partir de la spécification à tout moment, il cesse donc d'être un actif qui doit être maintenu et relu.
Exiger la preuve de non-ambiguïté en même temps que la preuve de correction coûte un travail supplémentaire au modèle mais transforme « cela semble correct » en une affirmation vérifiée par la machine.
Lorsque la génération est bon marché et la confiance rare, faites monter d'un niveau l'artefact humain : faites de la spécification le programme, faites du déterminisme une obligation de preuve, traitez le code comme un artefact de build jetable.
Suites
L'article, soumis à arXiv le 21 septembre 2026, démontre le paradigme sur plusieurs exemples et rapporte l'auto-hébergement : un LLM a implémenté le traducteur Djinnlang à partir de sa spécification et la réimplémentation s'est vérifiée elle-même. Les auteurs présentent ce résultat comme une forme forte de contrôle de l'IA — le modèle non fiable écrit, le vérificateur décide.
VÉRIFIEZ LES SOURCES