Eurydice is a compiler from Rust to C to provide a backwards-compatibility story as the verification ecosystem https://github.com/AeneasVerif/eurydice @rustlang #verification #C