Description:
Eurydice compiles (a decent subset of) Rust to C, enabling Rust-based verification while producing C code for legacy environments. It uses Charon and KaRaMeL passes to translate Rust into C, supporting compatibility with existing toolchains.