Programmierer schreiben zunehmend formale Spezifikationen und lassen LLMs diese implementieren, wobei jede Implementierung als zur Spezifikation passend bewiesen wird. Zu Ende gedacht werden Spezifikationssprachen zu den neuen Programmiersprachen – doch ein Problem blockiert den Wechsel: Zwei Programme können beide eine Spezifikation erfüllen und sich dennoch unterschiedlich verhalten, sodass jemand den generierten Code weiterhin lesen muss, um zu wissen, welches Verhalten man erhalten hat.
Djinnlangs Antwort ist eine Eindeutigkeitsbedingung. Zusätzlich zum Beweis, dass seine Implementierung die Spezifikation erfüllt, muss das LLM auch beweisen, dass jede andere Implementierung, die dieselbe Spezifikation erfüllt, bei identischen Eingaben identische Ausgaben erzeugen würde. Das schließt die Lücke: Der generierte Code muss nie gelesen werden und kann jederzeit aus der Spezifikation neu erzeugt werden, und ein nicht vertrauenswürdiges Modell kann Code schreiben, während ein Verifizierer seine Arbeit streng prüft.
Diese Anordnung macht das LLM effektiv zu einem Teil der Compiler-Toolchain. Ein Djinnlang-Programm besteht ausschließlich aus Spezifikationen – der Programmierer schreibt nie ausführbaren Code. Anstelle eines traditionellen Compilers senkt ein symbolischer Übersetzer jede Spezifikation zu Dafny-Stubs und Beweisverpflichtungen herab, und ein Treiber-Harness orchestriert ein LLM, das Implementierungen und Beweise ausfüllt, alles geprüft durch den Dafny-Verifizierer.
Als Beleg dafür, dass das Paradigma machbar ist, zeigen die Autoren, dass Djinnlang selbsthostend ist: Ein LLM implementierte den Djinnlang-Übersetzer aus dessen eigener Spezifikation, und die Neuimplementierung verifizierte sich selbst.
Beweise, dass die Spezifikation eindeutig ist, und lass dann ein nicht vertrauenswürdiges LLM das Compiler-Backend sein
Wenn sich alle Implementierungen einer Spezifikation identisch verhalten, liefert das Lesen des generierten Codes keine Information, auf die ein Programmierer reagieren könnte.
Der Beweis der Determinismus-Eigenschaft begrenzt, was das Modell ändern kann, sodass ein nicht vertrauenswürdiges Modell den Code schreiben kann, während der Verifizierer das Vertrauen trägt.
Verifizierter Code kann jederzeit aus der Spezifikation neu erzeugt werden, sodass er aufhört, ein Gut zu sein, das gepflegt und überprüft werden muss.
Den Eindeutigkeitsbeweis zusammen mit dem Korrektheitsbeweis zu verlangen, kostet das Modell zusätzliche Arbeit, verwandelt aber „sieht richtig aus“ in eine maschinell geprüfte Aussage.
Wenn die Generierung billig und Vertrauen knapp ist, verschiebe das menschliche Artefakt eine Ebene nach oben: Mach die Spezifikation zum Programm, mach Determinismus zu einer Beweisverpflichtung, behandle Code als wegwerfbares Build-Artefakt.
Das am 21. September 2026 bei arXiv eingereichte Paper demonstriert das Paradigma an mehreren Beispielen und berichtet von Selbsthosting: Ein LLM implementierte den Djinnlang-Übersetzer aus seiner Spezifikation, und die Neuimplementierung verifizierte sich selbst. Die Autoren rahmen das Ergebnis als eine starke Form der KI-Kontrolle ein – das nicht vertrauenswürdige Modell schreibt, der Verifizierer entscheidet.
DEN BELEGEN FOLGEN