Djinnlang put an LLM inside the compiler behind provably unambiguous specs

Programmers increasingly write formal specifications and let LLMs implement them, with each implementation proven to match its spec. Taken to that extreme, specification languages become the new programming languages — but one problem blocks the swap: two programs can both satisfy a spec and still behave differently, so someone still has to read the generated code to know which behavior they got.

Djinnlang's answer is an unambiguity constraint. In addition to proving its implementation satisfies the specification, the LLM must also prove that any other implementation satisfying the same spec would produce identical outputs on identical inputs. That closes the loophole: the generated code never needs to be read and can be regenerated from the spec at any time, and an untrusted model can write code while a verifier tightly checks its work.

The arrangement makes the LLM effectively part of the compiler toolchain. A Djinnlang program consists only of specifications — the programmer never writes executable code. In place of a traditional compiler, a symbolic translator lowers each spec to Dafny stubs and proof obligations, and a driver harness orchestrates an LLM that fills in implementations and proofs, all checked by the Dafny verifier.

As evidence the paradigm is feasible, the authors show Djinnlang is self-hosting: an LLM implemented the Djinnlang translator from its own specification, and the reimplementation verified itself.

If all implementations of a spec behave identically, reading the generated code adds no information a programmer could act on.

Proving determinism bounds what the model can change, so an untrusted model can write the code while the verifier carries the trust.

Verified code can be regenerated from the spec at any time, so it stops being an asset that has to be maintained and reviewed.

Requiring the unambiguity proof alongside the correctness proof costs the model extra work but converts 'looks right' into a machine-checked claim.

When generation is cheap and trust is scarce, move the human artifact up a level: make the spec the program, make determinism a proof obligation, treat code as a disposable build artifact.

The paper, submitted to arXiv on 21 September 2026, demonstrates the paradigm on multiple examples and reports self-hosting: an LLM implemented the Djinnlang translator from its specification and the reimplementation verified itself. The authors frame the result as a strong form of AI control — the untrusted model writes, the verifier decides.