rust-djinn: You Should Specify Your Code Unambiguously (and Prove That You Did)
Summary
The article introduces rust-djinn, a Rust macro-based system that allows specifying function behavior with constraints, which is then implemented by LLMs and verified with Lean via Aeneas. It discusses unambiguity constraints, the end-to-end workflow (cargo djinn implement and optimize), and benchmarks comparing a verified Gzip implementation against hand-optimized C, highlighting benefits and limitations of this approach. It also notes future work and provides links to the project and related papers.