Eurydice 是 Aeneas 项目内部开发的编译器，它将 Rust 源代码翻译为旨在可读且适用于验证工具期望 C 但 Rust 工具链不可用的环境中的 C 代码。该项目源自 Inria 与微软的合作，旨在作为验证生态系统逐步采用 Rust 的过渡方案，使新的 Rust 程序能够在仍依赖 C 基础分析的遗留环境中使用。
该编译器首先使用 Charon 工具从 rustc 提取 Rust 的中级中间表示（MIR）以 JSON 形式，然后将该 MIR 转换为 KaRaMeL 的内部抽象语法树。超过三十个纳米 pass 在此 AST 上运行，以消除没有直接 C 等价物的 Rust 特定构造，同时保持原始程序的求值顺序和结构；例如，一个简单的递归 GCD 函数被编译为 C 代码，并额外引入临时变量（如 uu____0）以强制与 Rust 源码相同的操作序列。为避免可能打乱此顺序的不需要的优化，生成的 C 代码必须使用 -fno-strict-aliasing 标志进行编译。
该图像显示了 Eurydice 项目的 GitHub 页面，该页面描述了编译器如何将 Rust 转换为 C，这与文章中对工具目的的解释相符。
Eurydice 目前仅处理 Rust 特性的一个子集；它在小型、自包含的程序上表现最佳，并且可能被诸如 const generics 之类的较新语言特性绊倒，这些特性会导致 Charon 在提取 MIR 时失败。此外，由于 Rust 的所有权和借用模型无法清晰映射到 C 的内存模型，翻译后的代码经常在技术上违反 C 的严格别名规则，因而需要上述编译器标志，有时会导致不够符合习惯的 C 输出，尽管该项目坚持认为原始 Rust 代码的语义在验证目的下得到了保存。