用 Djinn 写无歧义的代码规格并证明其正确性

rust-djinn 让开发者用接近 Rust 的语法直接写出形式化规格（如排序函数的长度、元素、有序性断言），由 LLM 生成代码并交给验证器证明实现与规格一致，无需手写算法。该工具基于 Aeneas（将 Rust 翻译为 Lean 等语言），目标是让普通软件工程师也能使用，而不必直接编写 Lean 代码或首次就写出完美规格。