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]; }
    }
}

No sorting algorithm. Just explaining what I am looking for.

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]; }
    }
}

Not a correct sorting spec.

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.

“challenge me to express myself unambiguously, so that you cannot misunderstand me anymore”

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:

• Mix specs into our normal Rust code
• Spawn agents at the press of a button and have them implement the specs
• Pretend our LLM is part of our compiler because we’ve verified everything it does and don’t need to read the code
• Hillclimb to get the fastest-possible implementation (also at the press of a button)
• Know that optimization won’t change what our code does, because the spec pins down a single behavior (except where specifically allowed)[3]

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;
}

Extracting data from an array, a single bit at a time. Not what optimized code traditionally looks like.

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):

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!

• I want to try this on more algorithms and codecs. There’s a great opportunity here to simplify some of the effort to move away from old, bug-ridden implementations and into safe Rust.
• Let’s build even better hill-climbing harnesses. My cargo djinn optimize is fairly naive; I am sure much could be improved on efficiency (both tokens and wall time) and optimization effectiveness.
• rust-djinn is currently research code[9] (and mostly vibe-coded, frankly) and I want to work on getting it ready for production environments.[10] This includes polishing the IDE support and LSP server to further lower the barrier to entry.

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

1. As Aeneas is being improved, that subset grows. ↩
2. “Substantially different” meaning no implementation that has different outputs given the same inputs, except where explicitly allowed in the spec. An example of allowing different outputs is the compression spec for Gzip: we want some output that round-trips, but we don’t want to prescribe the exact output bytes, because we want the model free to trade speed against compression ratio. ↩
3. Of course, your spec could still be wrong (though, in my experience, many bugs are caught either by the unambiguity constraint or because they make the spec contradictory). But you can at least expect that there will be no surprises as the LLM optimizes: the behavior of your code will be just as correct (or just as wrong) as it was in the first implementation. ↩
4. By the way, I don't mean to claim my LLM is a “superhuman” performance optimizer. All prior implementations were probably in the training data and the techniques the agents are trying seem very similar to theirs. Also, there is likely some overfitting to the target architecture and benchmark data, while those other implementations are carefully crafted to work well across many scenarios. I especially don't claim that my LLMs “invented” any new angles on Gzip decompression here, all the credit goes to the original authors who spent many hours optimizing. But (1) the hillclimbing seems very good at bringing out the best combinations among these existing techniques and (2) it is a very impressive feat that these LLMs can prove the optimizations correct. ↩
5. Decompression. CRC-32 checksum verification disabled where possible, including for both djinn-gzip and libdeflate. Measured on a Hetzner CCX43 cloud server: 16 dedicated vCPUs (8 cores, 16 threads) of an AMD EPYC Milan processor under KVM, with 32 MiB of L3 cache and 64 GB of RAM, running Ubuntu 26.04 with Linux 7.0. The machine ran nothing else during the measurements. Each benchmark was pinned to one logical CPU while its SMT sibling sat idle, and the benchmarks ran one after another. The guest cannot control CPU frequency, so turbo was left to the host. All Rust code (ours, zune_inflate 0.2.54, zlib-rs 0.6.6, miniz_oxide 0.8.9) was built with rustc 1.99.0 at 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. ↩
6. Non-blank lines, with comments (including doc comments) removed according to each language’s syntax. Braces, attributes and imports count as code. ↩
7. If you’re curious: the agents generated 845 lines of Rust and 8,861 lines of Lean proofs. No human programmer had to read or edit them. If you want to read them, they’re at https://github.com/shenniger/rust-djinn/tree/master/example/gzip/djinn ↩
8. And we shouldn't forget the many heroes who made it possible! It is an incredible accomplishment on the part of Rust's compiler team and the LLVM team that it is even at all possible to write safe Rust and beat hand-optimized C code. Their optimizer is doing a lot of work here. The LLMs are merely figuring out how to write Rust that best uses it. ↩
9. For instance, the current code base uses its own (probably buggy) semantics to translate Rust constraints to Lean. It should use Aeneas here. ↩
10. To get this ready for production, we also need to further improve the underlying tools so we can trust them. There are ongoing community efforts on this. ↩