I have a program that grants wishes, as long as I can state them precisely. Instead of implementing a Rust function, I describe what it should do, and the Djinn writes code that provably does exactly that. Suppose I want to sort a list. I write:
djinn! {
pub fn sort(v: &[i32]) -> r: Vec<i32> {
// My sorted list is the same length…
v.len() == r.len();
// … and it contains all the same elements …
for x in v { v.iter().filter(|y| y == x).count() == r.iter().filter(|y| y == x).count(); }
// … and it is sorted!
for i in 0..r.len() - 1 { r[i] <= r[i + 1]; }
}
}My Djinn is not magic, but it is the manifestation of a dream. People have wanted something like this for a long time: humans write specifications, then have LLMs implement them and prove to a verifier that their implementations are correct. In theory, this LLM-verifier combination is powerful (thanks to the LLM), but still safe and reliable so you don't need to read the resulting code (thanks to the verifier). In practice, it's a bit harder than it sounds. While the verifier provides certainty that the LLM's code matches our specification, it’s easy to make specification errors or underspecify. Also, you have to set up verification software (and establish trust boundaries), juggle different languages, and babysit agents. For this to land, it needs to be tractable for normal SWEs, and currently, it’s a pain even for formal methods experts.
What if there was an easy way for everyone to write formal specs in a somewhat familiar format, use LLMs for code implementation and optimization, and mix the resulting code with their regular project? One that works even for those who don’t want to touch Lean code directly or who don’t trust themselves to write a perfect spec on the first attempt?
That’s the Djinn — more precisely, rust-djinn.
Let’s build some tooling and a more pleasant syntax.
My approach builds on Aeneas, which translates Rust into Lean (and other proof assistants) so you can prove theorems about the original Rust code. Traditionally with Aeneas, we would write the specification in Lean. But that is not ideal — after all, we want our specified functions to tightly integrate with our existing Rust codebases.
That’s where rust-djinn comes in. It lets you specify a function within your existing Rust codebase using a djinn! macro. The Djinn has tooling that translates everything inside djinn! blocks into a Lean specification and implements it using an LLM. Within the blocks, you can use a subset of the normal Rust libraries and type system[1]. And once the LLM implementation is proven correct, it’s compiled and you can use the functions just like you would any other Rust code.
Within a djinn! block, the normal rules of imperative Rust programming don’t hold: we’re writing constraints. You can conceptualize the body as a long sequence of assert statements. Even the for loop is not an actual loop, but a universal quantifier (“for all items x in v, this constraint holds”). We write our code in a sort of relational programming language, constraining inputs and outputs. None of it is directly executable.
How do we turn this into executable code?
The tooling finds all djinn! blocks (which can be freely mixed into any Rust code base) and turns them into what we call “proof obligations” in Aeneas. A proof obligation is a theorem that must hold true about the (executable) code. With those proof obligations in hand, we spawn an LLM agent and ask it to (1) write Rust code that matches our spec, and (2) prove to us that it does so by fulfilling all proof obligations. We then ask Aeneas and Lean to check that our LLM’s proofs are correct, and finally we can compile the LLM’s Rust code with the regular Rust compiler.
This entire translation process happens in a single command: cargo djinn implement does everything from translation into Aeneas, spawning an LLM agent, babysitting it, and verifying that its work is correct. The programmer never has to touch Aeneas or Lean.
The newer LLMs are pretty good at this! They’re able to implement and prove even medium-sized specs of hundreds of lines (resulting in thousands of lines of code and much more in proofs) in a span of minutes to a few hours. Because we spawn an LLM agent, we can use the subscriptions (as opposed to API billing), making this remarkably cost-effective. And of course, we expect LLMs to get cheaper and better in the future.
Once we have the initial implementation, we make a benchmark for our measurements and run cargo djinn optimize. This optimizer is just an infinite loop that keeps spawning more and more agents which optimize the code. We can optimize for speed or for another target function: for instance, in compression, we also care about the compression factor. At every round of optimization, the agents need to prove their code is still correct and they need to demonstrate that it is faster on the benchmark. If it is not faster, it gets discarded, making this a classic instance of hillclimbing.
Within this framework, we can treat the LLM essentially as a compiler and we don’t have to review the code it wrote. We know what the spec is and we trust Lean to check it.
Any Rust programmer should be able to easily learn rust-djinn. It completely encapsulates both the LLM implementer agent and Lean/Aeneas; there is no need for the programmer to ever touch either. It also comes with some built-in protections to ensure that Rust never accidentally compiles a stale implementation or one that doesn't verify.
But what if we underspecify?
Think back to all those genie stories you may have heard as a kid. Your djinn fulfills your wishes, but not in the way you want because you don’t express yourself accurately enough.
The same problem exists in programming. What if our spec is wrong? How confident are we in our ability to write a good spec? In general, the answer is not very, and this is called the “spec elicitation problem” (Max von Hippel and Quinn Dougherty write about it at length here).
While bugs will always be a problem, a particular issue in this framework is actually underspecified code. What if we forget about something important? Suppose we forget to say that the output is a permutation of the input:
djinn! {
pub fn sort_broken(v: &[i32]) -> r: Vec<i32> {
// Sorting doesn’t change the length of my list…
v.len() == r.len();
// … and after sorting, the list is sorted
for i in 0..r.len() - 1 { r[i] <= r[i + 1]; }
}
}Now the function could always return a list of all zeros! Even if we trust the model to initially try to implement what we must have meant (which we probably shouldn’t), this kind of underspecification is a ticking time-bomb in an optimization loop.
The Unambiguity Constraint
What if your first wish for the Djinn could be: “for the following wishes, do what I mean, not what I say.” Well, it’s a bit unrealistic. The genie is powerful, but how would it know exactly what you want? Maybe you don’t even know yourself because you haven’t fully conceptualized it. So what if you could say: “challenge me to express myself unambiguously, so that you cannot misunderstand me anymore”?
That’s what we’re doing! rust-djinn automatically includes a proof obligation for spec unambiguity. So the model not only has to prove that its implementation matches the spec, but also that no substantially different implementation[2] would. Thus we can be relatively certain that the LLM has no leeway; with the unambiguity constraint, the verifier becomes a strong version of AI control.
The constraint makes the Djinn reject our wrong underbaked sorting spec and accept the correct one above. It also leads to something akin to “fighting the borrow checker”: a spec novice will be fighting the unambiguity constraint. If the human developer ever gets bored, they can enlist an LLM’s help. Turns out they’re pretty good at helping with writing specs too (just carefully check the results!).
Because it’s so common to fight the unambiguity constraint, I built a little smoke check that quickly tests for unambiguity on part of the search space and offers a counterexample when it is violated. I put this in a linter-style IDE plugin and it’s pretty fun to use.
For more details on unambiguity, read the academic paper I co-wrote with Stephen Chong and Nada Amin on an earlier dialect of Djinn (which used Dafny instead of Aeneas, but the concepts have remained similar).
Example: Gzip Spec
With this, we can now:
A few weeks ago, Kim Morrison wrote a brilliant blog article about how Lean is faster than Rust. She wrote a spec for gzip in Lean and had an LLM optimize the code (using Lean to prove that every step was correct) until it was faster than a Rust implementation. Of course, lean-gzip is not perfect. Kim herself acknowledges that her approach worked less well on decompression: even Rust baseline miniz_oxide is ~1.5x faster (and another Rust library, zune_inflate, is even faster, ~2.4x). It also uses a lot of bespoke tooling that doesn’t generalize to other workloads.
Let’s see how our approach does. I’ll start with decompression.
Using some LLM help, I translated Kim’s spec into Djinn. It’s less than 300 lines (including compression) and you can read it here on GitHub.
Nothing in the spec gives any indication at all that this code will be fast. We describe things like extracting individual bits by calling 2.pow. But that doesn’t matter too much. Because the spec only describes the relationship between inputs and outputs, any two ways of writing it that are logically equivalent lead to the same implementations. Writing it the slow-looking way shouldn’t cost anything, as long as the LLM can prove that its faster code satisfies the spec.
pub rel bit(s: &[u8], i: int) -> b: int {
0 <= i < 8 * s.len();
b == (s[i / 8] / 2.pow(i % 8)) % 2;
}Unlike Kim’s implementation, we also don’t add any external C or unsafe Rust functions for extra performance. Obviously, inline assembly and explicit vector instructions are also off-limits because Aeneas cannot verify them. We rely only on our LLM and the Rust compiler’s ability to optimize safe Rust code.
Given this spec, I used Codex and Claude Code (GPT 6 Astra at ultra and Fable 5.1 at xhigh) to optimize for 100 rounds (alternating between the two each round).
They optimized a bunch of stuff: 11-bit Huffman lookup tables built once per block, whole-token decoding from a single 64-bit bit window with packed table entries and the refill kept off the dependency chain, a pre-sized output buffer with unconditional 8-byte copy chunks, slice typing that lets LLVM drop bounds checks, and runtime-validated hints for long codes so proofs only need termination. They also tried a few things that didn't work: wider tables, branch-free or batched token decoding, overlapping-copy tricks for short distances, fusing literals into copies, out-of-line copies, and further polishing of the per-block setup.
And it turns out that the Djinn narrowly beats every other implementation[4] I tested so far (including zune_inflate, which claims to currently be the fastest safe Rust implementation):
| # | Decoder | MiB/s[5] | Human-Owned LoC[6] |
|---|---|---|---|
| — | memcpy (ceiling) | 31,752 | — |
| 1 | djinn-gzip | 787 | 277 (spec)[7] |
| 2 | libdeflate | 657 | 1,159 (1,793 with x86 SIMD) |
| 3 | zune_inflate | 652 | 1,413 |
| 4 | zlib-rs | 594 | 3,279 (5,323 with SIMD) |
| 5 | zlib-ng | 588 | 1,896 |
| 6 | miniz_oxide | 445 | 2,230 |
| 7 | zlib | 393 | 2,365 |
| 8 | lean-gzip | 283 | 322 (spec) |
| 9 | Zig | 227 | 1,285 |
| 10 | Go 1.26.3 | 203 | 1,411 |
| 11 | JS fflate | 111 | 2,154 (inflate + deflate, inseparable) |
| 12 | OCaml decompress | 98 | 4,763 (inflate + deflate, inseparable) |
Note that our headroom compared to libdeflate is fairly small and it could sometimes win depending on the dataset. Our benchmark also only tests a single setting (decoding a file that is already completely in memory), while the others are carefully constructed to support streaming. But that’s beside the point. The point isn’t to build a faster Gzip, but a verified Gzip in safe Rust that is no slower (or only insignificantly slower) than the fastest hand-optimized C implementation.[8]
I also tried this on compression. Compared to Kim’s lean-gzip, rust-djinn reaches similar compression ratios but is a bit slower for low compression levels and faster for higher ones. See details on this and the optimization process here on GitHub.
Next steps
I’m pretty excited about this and I want to try more things!
cargo djinn optimize is fairly naive; I am sure much could be improved on efficiency (both tokens and wall time) and optimization effectiveness.You can try rust-djinn yourself: https://github.com/shenniger/rust-djinn
This post is based on an academic paper I co-authored with Stephen Chong and Nada Amin. I am also grateful to Rhea Karty, Samuel Leßmann, and Max von Hippel for their comments.
Footnotes
opt-level = 3 with thin LTO, one codegen unit and panic = "abort", targeting baseline x86-64. zlib-ng 2.3.3 was compiled with gcc 16.2 at -O3. zlib 1.3.2 and libdeflate 1.25 are conda-forge builds, and libdeflate and zlib-ng select their x86 code paths at runtime. lean-gzip was built with Lean v4.33.0-rc1 and its own -O3 settings. Zig 0.14.1 was built in ReleaseFast mode and Go 1.26.3 with its defaults. fflate 0.8.3 ran on Node v26.10.0, and OCaml decompress 1.6.1 on OCaml 5.4.0 without flambda. Each figure is the geomean over Silesia files or streams, in MiB/s. ↩