I highly recommend checking out the other projects from AeneasVerif (and Jonathan Protzenko).

Scylla is kind of Eurydice's dual. But also Charon and the eponymous Aeneas.

Also, "There is ongoing work to integrate Eurydice-generated code for both Microsoft and Google’s respective crypto libraries." [1] which I find incredibly cool. This link is also a brilliant intro to Eurydice.

[1] https://jonathan.protzenko.fr/2025/10/28/eurydice.html