rust-djinn: You Should Specify Your Code Unambiguously (and Prove That You Did) henniger.dev

Simon Henniger introduces rust-djinn, a research tool that turns Rust specifications into LLM-generated implementations and uses Aeneas and Lean to verify both correctness and that the spec rules out different behaviors. In a gzip decompression benchmark, its safe Rust implementation reached 787 MiB/s, ahead of the tested alternatives, including libdeflate at 657 MiB/s; Henniger says the project is not yet ready for production.