I've been iterating on sodium bindings in Lean4 for about four months, and now that I've gotten to Ristretto255 I can see why the author is excited about its potential. Ristretto is a tightly designed API that allows me to build arbitrary polynomials on Curve25519 and I've been having a blast tinkering and experimenting with it! If the author by chance reads this, just want to say thank you for your work!