Eurydiceは、Aeneasプロジェクト内で開発されたコンパイラで、Rustのソースコードを人間が読めるCコードに変換し、検証ツールがCを期待するがRustツールチェーンが利用できない環境に適しています。InriaとMicrosoftの協業から生まれたこのプロジェクトは、検証エコシステムがRustを徐々に採用する中でのつなぎとして機能し、まだCベースの分析に依存しているレガシー環境でも新しいRustプログラムを使用できるようにすることを目的としています。
このコンパイラはまず、Charonツールを使ってrustcからRustの中間レベルの中間表現（MIR）をJSONとして抽出し、その後それをKaRaMeLの内部抽象構文木（AST）に変換します。その後、約30のナノパスがこのAST上で動作し、Cに直接対応する構造がないRust固有の構造を取り除きながら、元のプログラムの評価順序と構造を保持します。たとえば、単純な再帰GCD関数は、一時変数（uu____0など）を追加したCコードにコンパイルされ、Rustソースと同じ演算の順序を強制します。この順序を崩す不要な最適化を防ぐため、生成されたCコードは-fno-strict-aliasingフラグを付けてコンパイルする必要があります。
この画像は、EurydiceプロジェクトのGitHubページを示しており、コンパイラがRustをCに変換する方法が説明されており、記事でのツールの目的の説明と一致している。
現在、EurydiceはRustの機能の一部のみをサポートしており、小規模で独立したプログラムに最も適しています。const genericsなどの新しい言語機能では、CharonがMIRを抽出できずに失敗することがあります。さらに、Rustの所有権と借用モデルはCのメモリモデルにきれいにマッピングしないため、変換結果のコードはCの厳格エイリアシング規則を技術的に違反することが多く、前述のコンパイラフラグが必要になり、時には idiomatic でないCコードが生成されることがあります。ただし、プロジェクトは元のRustコードの意味が検証目的で保たれていると主張しています。