Checkout my latest post: [Formal Verification of secp256k1 modular scalar multiplication](https://remix7531.com/post/formal_verification_secp256k1_scalar_mul/)
Looking into the Software Foundations book a little bit. Interesting stuff, but seems like it would take a while to get competent with Rocq. Giving it a look though, as I've wanted to check out proof software for a while now.