A Vulnerability in Libsodium

Re:A Vulnerability in Libsodium by proof_by_vibes on Tuesday December 30, 2025 @02:25PM (#46436921)

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!

[ Parent | on HN ]

Re:A Vulnerability in Libsodium by fshacf on Tuesday December 30, 2025 @04:37PM (#46438319)

You have a public repo of this?

[ Parent | on HN ]

Re:A Vulnerability in Libsodium by proof_by_vibes on Tuesday December 30, 2025 @07:03PM (#46439766)

Yes: https://github.com/rj-calvin/sodium

The bindings are set and have a monadic interface, but there's some abstractions that still need refining/iterating: mostly I want to be able to formalize keyboard input and eventually build a tactic framework for zero-knowledge proofs.

[ Parent | on HN ]